Exact root degrees in the flat odd-prime-power extension

theorem MIPRE.LowDegree.BinaryPolynomial.flat_prime_power_minpoly {F : Type u_1} [Field F] (f : Polynomial F) (hf : f.Monic) (hi : Irreducible f) (q e : ℕ) (hq : Nat.Prime q) (hq2 : q ≠ 2) (hn : ∀ (b : AdjoinRoot f), b ^ q ≠ AdjoinRoot.root f) : minpoly F (AdjoinRoot.root (f.comp (Polynomial.X ^ q ^ e))) = f.comp (Polynomial.X ^ q ^ e)

The flat extension root has the full specified minimal polynomial.

theorem MIPRE.LowDegree.BinaryPolynomial.flat_prime_power_root_pow_minpoly {F : Type u_1} [Field F] (f : Polynomial F) (hf : f.Monic) (hi : Irreducible f) (q e : ℕ) (hq : Nat.Prime q) (hq2 : q ≠ 2) (hn : ∀ (b : AdjoinRoot f), b ^ q ≠ AdjoinRoot.root f) : minpoly F (AdjoinRoot.root (f.comp (Polynomial.X ^ q ^ (e + 1))) ^ q) = f.comp (Polynomial.X ^ q ^ e)

Raising the flat extension generator to the base prime removes exactly one prime-power level from its minimal polynomial.