Irreducibility of the flat odd-prime-power extension

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

A nonresidue at the specified quotient root suffices for every odd-prime-power composition, through the canonical isomorphism with any other simple root field.

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

The next substitution is reducible only if the current root is a residue.