feat: Criteria for X ^ n - C a to be irreducible for odd n. (#9397)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Mathlib/Algebra/GroupWithZero/Power.lean

@@ -5,6 +5,7 @@ Authors: Johan Commelin
 -/
 import Mathlib.Algebra.GroupPower.Lemmas
 import Mathlib.Util.AssertExists
+import Mathlib.Data.Int.GCD
 
 #align_import algebra.group_with_zero.power from "leanprover-community/mathlib"@"46a64b5b4268c594af770c44d9e502afc6a515cb"
 
@@ -171,6 +172,24 @@ theorem zpow_neg_mul_zpow_self (n : ℤ) {x : G₀} (h : x ≠ 0) : x ^ (-n) * x
   exact inv_mul_cancel (zpow_ne_zero n h)
 #align zpow_neg_mul_zpow_self zpow_neg_mul_zpow_self
 
+lemma Commute.exists_eq_pow_of_pow_eq_pow_of_coprime {a b : G₀} (h : Commute a b) {m n : ℕ}
+    (hmn : m.Coprime n) (hab : a ^ m = b ^ n) :
+    ∃ c, a = c ^ n ∧ b = c ^ m := by
+  by_cases hn : n = 0; · aesop
+  by_cases hm : m = 0; · aesop
+  by_cases hb : b = 0; exact ⟨0, by aesop⟩
+  by_cases ha : a = 0; exact ⟨0, by have := hab.symm; aesop⟩
+  use a ^ (Nat.gcdB m n) * b ^ (Nat.gcdA m n)
+  constructor
+  all_goals
+    refine (pow_one _).symm.trans ?_
+    conv_lhs => rw [← zpow_ofNat, ← hmn, Nat.gcd_eq_gcd_ab]
+    simp only [zpow_add₀ ha, zpow_add₀ hb, ← zpow_ofNat, (h.zpow_zpow₀ _ _).mul_zpow, ← zpow_mul,
+      mul_comm (Nat.gcdB m n), mul_comm (Nat.gcdA m n)]
+    simp only [zpow_mul, zpow_ofNat, hab]
+    refine ((Commute.pow_pow ?_ _ _).zpow_zpow₀ _ _).symm
+    aesop
+
 end ZPow
 
 section
@@ -183,6 +202,15 @@ theorem div_sq_cancel (a b : G₀) : a ^ 2 * b / a = a * b := by
   rw [sq, mul_assoc, mul_div_cancel_left _ ha]
 #align div_sq_cancel div_sq_cancel
 
+theorem pow_mem_range_pow_of_coprime {m n : ℕ} (hmn : m.Coprime n) (a : G₀) :
+    a ^ m ∈ Set.range (· ^ n : G₀ → G₀) ↔ a ∈ Set.range (· ^ n : G₀ → G₀) := by
+  constructor
+  · intro ⟨x, hx⟩
+    obtain ⟨c, rfl, rfl⟩ := (Commute.all x a).exists_eq_pow_of_pow_eq_pow_of_coprime hmn.symm hx
+    exact ⟨c, rfl⟩
+  · rintro ⟨x, rfl⟩
+    exact ⟨x ^ m, by simp [← pow_mul, mul_comm m n]⟩
+
 end
 
 -- Guard against import creep regression.

Mathlib/Data/Polynomial/RingDivision.lean

@@ -1264,6 +1264,37 @@ theorem leadingCoeff_divByMonic_X_sub_C (p : R[X]) (hp : degree p ≠ 0) (a : R)
 set_option linter.uppercaseLean3 false in
 #align polynomial.leading_coeff_div_by_monic_X_sub_C Polynomial.leadingCoeff_divByMonic_X_sub_C
 
+theorem eq_of_dvd_of_natDegree_le_of_leadingCoeff {p q : R[X]} (hpq : p ∣ q)
+    (h₁ : q.natDegree ≤ p.natDegree) (h₂ : p.leadingCoeff = q.leadingCoeff) :
+    p = q := by
+  by_cases hq : q = 0
+  · rwa [hq, leadingCoeff_zero, leadingCoeff_eq_zero, ← hq] at h₂
+  replace h₁ := (natDegree_le_of_dvd hpq hq).antisymm h₁
+  obtain ⟨u, rfl⟩ := hpq
+  replace hq := mul_ne_zero_iff.mp hq
+  rw [natDegree_mul hq.1 hq.2, self_eq_add_right] at h₁
+  rw [eq_C_of_natDegree_eq_zero h₁, leadingCoeff_mul, leadingCoeff_C,
+    eq_comm, mul_eq_left₀ (leadingCoeff_ne_zero.mpr hq.1)] at h₂
+  rw [eq_C_of_natDegree_eq_zero h₁, h₂, map_one, mul_one]
+
+theorem associated_of_dvd_of_natDegree_le_of_leadingCoeff {p q : R[X]} (hpq : p ∣ q)
+    (h₁ : q.natDegree ≤ p.natDegree) (h₂ : q.leadingCoeff ∣ p.leadingCoeff) :
+    Associated p q :=
+  have ⟨r, hr⟩ := hpq
+  have ⟨u, hu⟩ := associated_of_dvd_dvd ⟨leadingCoeff r, hr ▸ leadingCoeff_mul p r⟩ h₂
+  ⟨Units.map C.toMonoidHom u, eq_of_dvd_of_natDegree_le_of_leadingCoeff
+    (by rwa [Units.mul_right_dvd]) (by simpa [natDegree_mul_C] using h₁) (by simpa using hu)⟩
+
+theorem associated_of_dvd_of_natDegree_le {K} [Field K] {p q : K[X]} (hpq : p ∣ q) (hq : q ≠ 0)
+    (h₁ : q.natDegree ≤ p.natDegree) : Associated p q :=
+  associated_of_dvd_of_natDegree_le_of_leadingCoeff hpq h₁
+    (IsUnit.dvd (by rwa [← leadingCoeff_ne_zero, ← isUnit_iff_ne_zero] at hq))
+
+theorem associated_of_dvd_of_degree_eq {K} [Field K] {p q : K[X]} (hpq : p ∣ q)
+    (h₁ : p.degree = q.degree) : Associated p q :=
+  (Classical.em (q = 0)).elim (fun hq ↦ (show p = q by simpa [hq] using h₁) ▸ Associated.refl p)
+    (associated_of_dvd_of_natDegree_le hpq · (natDegree_le_natDegree h₁.ge))
+
 theorem eq_leadingCoeff_mul_of_monic_of_dvd_of_natDegree_le {R} [CommRing R] {p q : R[X]}
     (hp : p.Monic) (hdiv : p ∣ q) (hdeg : q.natDegree ≤ p.natDegree) :
     q = C q.leadingCoeff * p := by

Mathlib/FieldTheory/Adjoin.lean

@@ -558,6 +558,9 @@ def AdjoinSimple.gen : F⟮α⟯ :=
 #align intermediate_field.adjoin_simple.gen IntermediateField.AdjoinSimple.gen
 
 @[simp]
+theorem AdjoinSimple.coe_gen : (AdjoinSimple.gen F α : E) = α :=
+  rfl
+
 theorem AdjoinSimple.algebraMap_gen : algebraMap F⟮α⟯ E (AdjoinSimple.gen F α) = α :=
   rfl
 #align intermediate_field.adjoin_simple.algebra_map_gen IntermediateField.AdjoinSimple.algebraMap_gen
@@ -866,6 +869,12 @@ theorem finrank_bot : finrank F (⊥ : IntermediateField F E) = 1 := by rw [finr
 @[simp] protected theorem finrank_top : finrank (⊤ : IntermediateField F E) E = 1 :=
   rank_eq_one_iff_finrank_eq_one.mp IntermediateField.rank_top
 
+@[simp] theorem rank_top' : Module.rank F (⊤ : IntermediateField F E) = Module.rank F E :=
+  rank_top F E
+
+@[simp] theorem finrank_top' : finrank F (⊤ : IntermediateField F E) = finrank F E :=
+  finrank_top F E
+
 theorem rank_adjoin_eq_one_iff : Module.rank F (adjoin F S) = 1 ↔ S ⊆ (⊥ : IntermediateField F E) :=
   Iff.trans rank_eq_one_iff adjoin_eq_bot_iff
 #align intermediate_field.rank_adjoin_eq_one_iff IntermediateField.rank_adjoin_eq_one_iff
@@ -926,9 +935,11 @@ end AdjoinIntermediateFieldLattice
 
 section AdjoinIntegralElement
 
+universe u
+
 variable (F : Type*) [Field F] {E : Type*} [Field E] [Algebra F E] {α : E}
 
-variable {K : Type*} [Field K] [Algebra F K]
+variable {K : Type u} [Field K] [Algebra F K]
 
 theorem minpoly_gen (α : E) :
     minpoly F (AdjoinSimple.gen F α) = minpoly F α := by
@@ -974,6 +985,9 @@ theorem adjoinRootEquivAdjoin_apply_root (h : IsIntegral F α) :
   AdjoinRoot.lift_root (aeval_gen_minpoly F α)
 #align intermediate_field.adjoin_root_equiv_adjoin_apply_root IntermediateField.adjoinRootEquivAdjoin_apply_root
 
+theorem adjoin_root_eq_top (p : K[X]) [Fact (Irreducible p)] : K⟮AdjoinRoot.root p⟯ = ⊤ :=
+  (eq_adjoin_of_eq_algebra_adjoin K _ ⊤ (AdjoinRoot.adjoinRoot_eq_top (f := p)).symm).symm
+
 section PowerBasis
 
 variable {L : Type*} [Field L] [Algebra K L]
@@ -1133,6 +1147,56 @@ theorem card_algHom_adjoin_integral (h : IsIntegral F α) (h_sep : (minpoly F α
     simp only [adjoin.powerBasis_dim, adjoin.powerBasis_gen, minpoly_gen, h_sep, h_splits]
 #align intermediate_field.card_alg_hom_adjoin_integral IntermediateField.card_algHom_adjoin_integral
 
+open FiniteDimensional AdjoinRoot in
+/-- Let `f, g` be monic polynomials over `K`. If `f` is irreducible, and `g(x) - α` is irreducible
+in `K⟮α⟯` with `α` a root of `f`, then `f(g(x))` is irreducible. -/
+theorem _root_.Polynomial.irreducible_comp {f g : K[X]} (hfm : f.Monic) (hgm : g.Monic)
+    (hf : Irreducible f)
+    (hg : ∀ (E : Type u) [Field E] [Algebra K E] (x : E) (hx : minpoly K x = f),
+      Irreducible (g.map (algebraMap _ _) - C (AdjoinSimple.gen K x))) :
+    Irreducible (f.comp g) := by
+  have hf' : natDegree f ≠ 0 :=
+    fun e ↦ not_irreducible_C (f.coeff 0) (eq_C_of_natDegree_eq_zero e ▸ hf)
+  have hg' : natDegree g ≠ 0
+  · have := Fact.mk hf
+    intro e
+    apply not_irreducible_C ((g.map (algebraMap _ _)).coeff 0 - AdjoinSimple.gen K (root f))
+    rw [map_sub, coeff_map, ← map_C, ← eq_C_of_natDegree_eq_zero e]
+    apply hg (AdjoinRoot f)
+    rw [AdjoinRoot.minpoly_root hf.ne_zero, hfm, inv_one, map_one, mul_one]
+  have H₁ : f.comp g ≠ 0 := fun h ↦ by simpa [hf', hg', natDegree_comp] using congr_arg natDegree h
+  have H₂ : ¬ IsUnit (f.comp g) := fun h ↦
+    by simpa [hf', hg', natDegree_comp] using natDegree_eq_zero_of_isUnit h
+  have ⟨p, hp₁, hp₂⟩ := WfDvdMonoid.exists_irreducible_factor H₂ H₁
+  suffices natDegree p = natDegree f * natDegree g from (associated_of_dvd_of_natDegree_le hp₂ H₁
+    (this.trans natDegree_comp.symm).ge).irreducible hp₁
+  have := Fact.mk hp₁
+  let Kx := AdjoinRoot p
+  letI := (AdjoinRoot.powerBasis hp₁.ne_zero).finiteDimensional
+  have key₁ : f = minpoly K (aeval (root p) g)
+  · refine minpoly.eq_of_irreducible_of_monic hf ?_ hfm
+    rw [← aeval_comp]
+    exact aeval_eq_zero_of_dvd_aeval_eq_zero hp₂ (AdjoinRoot.eval₂_root p)
+  have key₁' : finrank K K⟮aeval (root p) g⟯ = natDegree f
+  · rw [adjoin.finrank, ← key₁]
+    exact IsIntegral.of_finite _ _
+  have key₂ : g.map (algebraMap _ _) - C (AdjoinSimple.gen K (aeval (root p) g)) =
+      minpoly K⟮aeval (root p) g⟯ (root p)
+  · exact minpoly.eq_of_irreducible_of_monic (hg _ _ key₁.symm) (by simp [AdjoinSimple.gen])
+      (Monic.sub_of_left (hgm.map _) (degree_lt_degree (by simpa [Nat.pos_iff_ne_zero] using hg')))
+  have key₂' : finrank K⟮aeval (root p) g⟯ Kx = natDegree g
+  · trans natDegree (minpoly K⟮aeval (root p) g⟯ (root p))
+    · have : K⟮aeval (root p) g⟯⟮root p⟯ = ⊤
+      · apply restrictScalars_injective K
+        rw [restrictScalars_top, adjoin_adjoin_left, Set.union_comm, ← adjoin_adjoin_left,
+          adjoin_root_eq_top p, restrictScalars_adjoin]
+        simp
+      rw [← finrank_top', ← this, adjoin.finrank]
+      exact IsIntegral.of_finite _ _
+    · simp [← key₂]
+  have := FiniteDimensional.finrank_mul_finrank K K⟮aeval (root p) g⟯ Kx
+  rwa [key₁', key₂', (AdjoinRoot.powerBasis hp₁.ne_zero).finrank, powerBasis_dim, eq_comm] at this
+
 end AdjoinIntegralElement
 
 section Induction

Mathlib/FieldTheory/IntermediateField.lean

@@ -387,6 +387,10 @@ instance toAlgebra {R : Type*} [Semiring R] [Algebra L R] : Algebra S R :=
   S.toSubalgebra.toAlgebra
 #align intermediate_field.to_algebra IntermediateField.toAlgebra
 
+@[simp] lemma algebraMap_apply (x : S) : algebraMap S L x = x := rfl
+
+@[simp] lemma coe_algebraMap_apply (x : K) : ↑(algebraMap K S x) = algebraMap K L x := rfl
+
 instance isScalarTower_bot {R : Type*} [Semiring R] [Algebra L R] : IsScalarTower S L R :=
   IsScalarTower.subalgebra _ _ _ S.toSubalgebra
 #align intermediate_field.is_scalar_tower_bot IntermediateField.isScalarTower_bot

Mathlib/FieldTheory/KummerExtension.lean

@@ -8,6 +8,7 @@ import Mathlib.RingTheory.AdjoinRoot
 import Mathlib.LinearAlgebra.Charpoly.Basic
 import Mathlib.FieldTheory.Galois
 import Mathlib.LinearAlgebra.Eigenspace.Minpoly
+import Mathlib.RingTheory.Norm
 /-!
 # Kummer Extensions
 
@@ -31,12 +32,21 @@ then isomorphic to `Multiplicative (ZMod n)` whose inverse is given by
 
 ## Other results
 Criteria for `X ^ n - C a` to be irreducible is given:
-- `X_pow_sub_C_irreducible_iff_of_prime`: `X ^ n - C a` is irreducible iff `a` is not a `p`-power.
+- `X_pow_sub_C_irreducible_iff_of_prime`:
+  For `n = p` a prime, `X ^ n - C a` is irreducible iff `a` is not a `p`-power.
+- `X_pow_sub_C_irreducible_iff_of_prime_pow`:
+  For `n = p ^ k` an odd prime power, `X ^ n - C a` is irreducible iff `a` is not a `p`-power.
+- `X_pow_sub_C_irreducible_iff_forall_prime_of_odd`:
+  For `n` odd, `X ^ n - C a` is irreducible iff `a` is not a `p`-power for all prime `p ∣ n`.
+- `X_pow_sub_C_irreducible_iff_of_odd`:
+  For `n` odd, `X ^ n - C a` is irreducible iff `a` is not a `d`-power for `d ∣ n` and `d ≠ 1`.
 
-TODO: criteria for general `n`. See [serge_lang_algebra] VI,§9.
+TODO: criteria for even `n`. See [serge_lang_algebra] VI,§9.
 
 -/
-variable {K : Type*} [Field K]
+universe u
+
+variable {K : Type u} [Field K]
 
 open Polynomial IntermediateField AdjoinRoot
 
@@ -109,6 +119,115 @@ lemma root_X_pow_sub_C_ne_zero_iff {n : ℕ} {a : K} (H : Irreducible (X ^ n - C
     (AdjoinRoot.root (X ^ n - C a)) ≠ 0 ↔ a ≠ 0 :=
   (root_X_pow_sub_C_eq_zero_iff H).not
 
+theorem pow_ne_of_irreducible_X_pow_sub_C {n : ℕ} {a : K}
+    (H : Irreducible (X ^ n - C a)) {m : ℕ} (hm : m ∣ n) (hm' : m ≠ 1) (b : K) : b ^ m ≠ a := by
+  have hn : n ≠ 0 := fun e ↦ not_irreducible_C
+    (1 - a) (by simpa only [e, pow_zero, ← C.map_one, ← map_sub] using H)
+  obtain ⟨k, rfl⟩ := hm
+  rintro rfl
+  obtain ⟨q, hq⟩ := sub_dvd_pow_sub_pow (X ^ k) (C b) m
+  rw [mul_comm, pow_mul, map_pow, hq] at H
+  have : degree q = 0
+  · simpa [isUnit_iff_degree_eq_zero, degree_X_pow_sub_C,
+      Nat.pos_iff_ne_zero, (mul_ne_zero_iff.mp hn).2] using H.2 _ q rfl
+  apply_fun degree at hq
+  simp only [this, ← pow_mul, mul_comm k m, degree_X_pow_sub_C, Nat.pos_iff_ne_zero.mpr hn,
+    Nat.pos_iff_ne_zero.mpr (mul_ne_zero_iff.mp hn).2, degree_mul, ← map_pow, add_zero,
+    Nat.cast_injective.eq_iff] at hq
+  exact hm' ((mul_eq_right₀ (mul_ne_zero_iff.mp hn).2).mp hq)
+
+theorem X_pow_sub_C_irreducible_of_prime {p : ℕ} (hp : p.Prime) {a : K} (ha : ∀ b : K, b ^ p ≠ a) :
+    Irreducible (X ^ p - C a) := by
+  -- First of all, We may find an irreducible factor `g` of `X ^ p - C a`.
+  have : ¬ IsUnit (X ^ p - C a)
+  · rw [Polynomial.isUnit_iff_degree_eq_zero, degree_X_pow_sub_C hp.pos, Nat.cast_eq_zero]
+    exact hp.ne_zero
+  have ⟨g, hg, hg'⟩ := WfDvdMonoid.exists_irreducible_factor this (X_pow_sub_C_ne_zero hp.pos a)
+  -- It suffices to show that `deg g = p`.
+  suffices natDegree g = p from (associated_of_dvd_of_natDegree_le hg'
+    (X_pow_sub_C_ne_zero hp.pos a) (this.trans natDegree_X_pow_sub_C.symm).ge).irreducible hg
+  -- Suppose `deg g ≠ p`.
+  by_contra h
+  have : Fact (Irreducible g) := ⟨hg⟩
+  -- Let `r` be a root of `g`, then `N_K(r) ^ p = N_K(r ^ p) = N_K(a) = a ^ (deg g)`.
+  have key : (Algebra.norm K (AdjoinRoot.root g)) ^ p = a ^ g.natDegree
+  · have := eval₂_eq_zero_of_dvd_of_eval₂_eq_zero _ _ hg' (AdjoinRoot.eval₂_root g)
+    rw [eval₂_sub, eval₂_pow, eval₂_C, eval₂_X, sub_eq_zero] at this
+    rw [← map_pow, this, ← AdjoinRoot.algebraMap_eq, Algebra.norm_algebraMap,
+      ← finrank_top', ← IntermediateField.adjoin_root_eq_top g,
+      IntermediateField.adjoin.finrank,
+      AdjoinRoot.minpoly_root hg.ne_zero, natDegree_mul_C]
+    · simpa using hg.ne_zero
+    · exact AdjoinRoot.isIntegral_root hg.ne_zero
+  -- Since `a ^ (deg g)` is a `p`-power, and `p` is coprime to `deg g`, we conclude that `a` is
+  -- also a `p`-power, contradicting the hypothesis
+  have : p.Coprime (natDegree g) := hp.coprime_iff_not_dvd.mpr (fun e ↦ h (((natDegree_le_of_dvd hg'
+    (X_pow_sub_C_ne_zero hp.pos a)).trans_eq natDegree_X_pow_sub_C).antisymm (Nat.le_of_dvd
+      (natDegree_pos_iff_degree_pos.mpr <| Polynomial.degree_pos_of_irreducible hg) e)))
+  exact ha _ ((pow_mem_range_pow_of_coprime this.symm a).mp ⟨_, key⟩).choose_spec
+
+theorem X_pow_sub_C_irreducible_iff_of_prime {p : ℕ} (hp : p.Prime) {a : K} :
+    Irreducible (X ^ p - C a) ↔ ∀ b, b ^ p ≠ a :=
+  ⟨(pow_ne_of_irreducible_X_pow_sub_C · dvd_rfl hp.ne_one), X_pow_sub_C_irreducible_of_prime hp⟩
+
+theorem X_pow_mul_sub_C_irreducible
+    {n m : ℕ} {a : K} (hm : Irreducible (X ^ m - C a))
+    (hn : ∀ (E : Type u) [Field E] [Algebra K E] (x : E) (hx : minpoly K x = X ^ m - C a),
+      Irreducible (X ^ n - C (AdjoinSimple.gen K x))) :
+    Irreducible (X ^ (n * m) - C a) := by
+  have hm' : m ≠ 0
+  · rintro rfl
+    rw [pow_zero, ← C.map_one, ← map_sub] at hm
+    exact not_irreducible_C _ hm
+  simpa [pow_mul] using irreducible_comp (monic_X_pow_sub_C a hm') (monic_X_pow n) hm
+    (by simpa only [Polynomial.map_pow, map_X] using hn)
+
+-- TODO: generalize to even `n`
+theorem X_pow_sub_C_irreducible_of_odd
+    {n : ℕ} (hn : Odd n) {a : K} (ha : ∀ p : ℕ, p.Prime → p ∣ n → ∀ b : K, b ^ p ≠ a) :
+    Irreducible (X ^ n - C a) := by
+  induction n using induction_on_primes generalizing K a with
+  | h₀ => simp at hn
+  | h₁ => simpa using irreducible_X_sub_C a
+  | h p n hp IH =>
+    rw [mul_comm]
+    apply X_pow_mul_sub_C_irreducible
+      (X_pow_sub_C_irreducible_of_prime hp (ha p hp (dvd_mul_right _ _)))
+    intro E _ _ x hx
+    have : IsIntegral K x := not_not.mp fun h ↦ by
+      simpa only [degree_zero, degree_X_pow_sub_C hp.pos,
+        WithBot.nat_ne_bot] using congr_arg degree (hx.symm.trans (dif_neg h))
+    apply IH (Nat.odd_mul.mp hn).2
+    intros q hq hqn b hb
+    apply ha q hq (dvd_mul_of_dvd_right hqn p) (Algebra.norm _ b)
+    rw [← map_pow, hb, ← adjoin.powerBasis_gen this,
+      Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly]
+    simp [minpoly_gen, hx, hp.ne_zero.symm, (Nat.odd_mul.mp hn).1.neg_pow]
+
+theorem X_pow_sub_C_irreducible_iff_forall_prime_of_odd {n : ℕ} (hn : Odd n) {a : K} :
+    Irreducible (X ^ n - C a) ↔ (∀ p : ℕ, p.Prime → p ∣ n → ∀ b : K, b ^ p ≠ a) :=
+  ⟨fun e _ hp hpn ↦ pow_ne_of_irreducible_X_pow_sub_C e hpn hp.ne_one,
+    X_pow_sub_C_irreducible_of_odd hn⟩
+
+theorem X_pow_sub_C_irreducible_iff_of_odd {n : ℕ} (hn : Odd n) {a : K} :
+    Irreducible (X ^ n - C a) ↔ (∀ d, d ∣ n → d ≠ 1 → ∀ b : K, b ^ d ≠ a) :=
+  ⟨fun e _ ↦ pow_ne_of_irreducible_X_pow_sub_C e,
+    fun H ↦ X_pow_sub_C_irreducible_of_odd hn fun p hp hpn ↦ (H p hpn hp.ne_one)⟩
+
+-- TODO: generalize to `p = 2`
+theorem X_pow_sub_C_irreducible_of_prime_pow
+    {p : ℕ} (hp : p.Prime) (hp' : p ≠ 2) (n : ℕ) {a : K} (ha : ∀ b : K, b ^ p ≠ a) :
+    Irreducible (X ^ (p ^ n) - C a) := by
+  apply X_pow_sub_C_irreducible_of_odd (hp.odd_of_ne_two hp').pow
+  intros q hq hq'
+  simpa [(Nat.prime_dvd_prime_iff_eq hq hp).mp (hq.dvd_of_dvd_pow hq')] using ha
+
+theorem X_pow_sub_C_irreducible_iff_of_prime_pow
+    {p : ℕ} (hp : p.Prime) (hp' : p ≠ 2) {n} (hn : n ≠ 0) {a : K} :
+    Irreducible (X ^ p ^ n - C a) ↔ ∀ b, b ^ p ≠ a :=
+  ⟨(pow_ne_of_irreducible_X_pow_sub_C · (dvd_pow dvd_rfl hn) hp.ne_one),
+    X_pow_sub_C_irreducible_of_prime_pow hp hp' n⟩
+
 end Irreducible
 
 /-!