feat(FieldTheory/Finite): irreducible polynomial divides X^q^n - X iff degree divides n

Mathlib/FieldTheory/Finite/Extension.lean

@@ -174,4 +174,32 @@ theorem Irreducible.natDegree_dvd_of_dvd_X_pow_card_pow_sub_X {n : ℕ} {f : K[X
   · apply IsSplittingField.splits
   · exact map_ne_zero (X_pow_card_pow_sub_X_ne_zero K hn Finite.one_lt_card)
 
+theorem Irreducible.dvd_X_pow_card_pow_natDegree_sub_X [Finite K] {f : K[X]}
+   (hi : Irreducible f) : f ∣ X ^ (Nat.card K) ^ f.natDegree - X := by
+  let a := AdjoinRoot.root f
+  have : NeZero f.natDegree := NeZero.of_pos (Irreducible.natDegree_pos hi)
+  have : Fact <| Irreducible f := ⟨hi⟩
+  refine Irreducible.dvd_of_aeval_eq_zero hi (b := a) ?_ ?_
+  · rw [Polynomial.aeval_def]
+    exact AdjoinRoot.eval₂_root f
+  · let ⟨p, hp⟩ := CharP.exists K
+    have : Fact (Nat.Prime p) := ⟨CharP.char_is_prime K p⟩
+    let e := FiniteField.algEquivExtension K p f.natDegree (AdjoinRoot f)
+      (finrank_quotient_span_eq_natDegree (f := f))
+    have hpeval : (e a) ^ (Nat.card K) ^ f.natDegree - (e a) = 0 := by
+      have := Fintype.ofFinite (Extension K p f.natDegree)
+      rw [← (natCard_extension K p f.natDegree), ← Fintype.card_eq_nat_card,
+        pow_card (e a), sub_self]
+    apply_fun e.symm at hpeval
+    simpa using hpeval
+
+lemma Irreducible.dvd_X_pow_card_pow_sub_X_of_natDegree_dvd [Finite K] {n : ℕ} {f : K[X]}
+    (hi : Irreducible f) (hdvd : f.natDegree ∣ n) : f ∣ X ^ (Nat.card K) ^ n - X  :=
+  dvd_trans (Irreducible.dvd_X_pow_card_pow_natDegree_sub_X hi) (dvd_pow_pow_sub_self_of_dvd hdvd)
+
+theorem Irreducible.natDegree_dvd_iff_dvd_X_pow_card_pow_sub_X [Finite K] {n : ℕ} {f : K[X]}
+    (hi : Irreducible f) : f.natDegree ∣ n ↔ f ∣ X ^ (Nat.card K) ^ n - X  :=
+  ⟨Irreducible.dvd_X_pow_card_pow_sub_X_of_natDegree_dvd hi,
+    Irreducible.natDegree_dvd_of_dvd_X_pow_card_pow_sub_X hi⟩
+
 end Polynomial

Mathlib/FieldTheory/Minpoly/Field.lean

@@ -166,6 +166,12 @@ theorem Irreducible.eq_minpoly [Nontrivial B] {p : A[X]} (hi : Irreducible p)
   rw [← minpoly.eq_of_irreducible hi hx, mul_comm, mul_assoc, ← C_mul,
     inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr hi.ne_zero), C_1, mul_one]
 
+theorem _root_.Irreducible.dvd_of_aeval_eq_zero [Nontrivial B] {p q : A[X]} (hi : Irreducible p)
+    {b : B} (hfa : p.aeval b = 0) (hga : q.aeval b = 0) : p ∣ q := by
+  refine dvd_trans ?_ (minpoly.dvd A b hga)
+  rw [← minpoly.eq_of_irreducible hi hfa]
+  exact dvd_mul_right _ _
+
 theorem add_algebraMap {B : Type*} [CommRing B] [Algebra A B] (x : B)
     (a : A) : minpoly A (x + algebraMap A B a) = (minpoly A x).comp (X - C a) := by
   by_cases hx : IsIntegral A x