English
If f ∈ F[X] is irreducible and p ≠ 0, there exist n and g ∈ F[X] with g Separable and expand F(p^n) g = f.
Русский
Если f ∈ F[X] неприводим и p ≠ 0, существует n и g ∈ F[X] such that g сепарабелен и expand F(p^n) g = f.
LaTeX
$$$\\exists n, g: F[X], g\\;Separable \\land \\text{expand}_F(p^n)(g) = f$$$
Lean4
theorem exists_separable_of_irreducible {f : F[X]} (hf : Irreducible f) (hp : p ≠ 0) :
∃ (n : ℕ) (g : F[X]), g.Separable ∧ expand F (p ^ n) g = f :=
by
replace hp : p.Prime := (CharP.char_is_prime_or_zero F p).resolve_right hp
induction hn : f.natDegree using Nat.strong_induction_on generalizing f with
| _ N ih
rcases separable_or p hf with (h | ⟨h1, g, hg, hgf⟩)
· refine ⟨0, f, h, ?_⟩
rw [pow_zero, expand_one]
· rcases N with - | N
· rw [natDegree_eq_zero_iff_degree_le_zero, degree_le_zero_iff] at hn
rw [hn, separable_C, isUnit_iff_ne_zero, Classical.not_not] at h1
have hf0 : f ≠ 0 := hf.ne_zero
rw [h1, C_0] at hn
exact absurd hn hf0
have hg1 : g.natDegree * p = N.succ := by rwa [← natDegree_expand, hgf]
have hg2 : g.natDegree ≠ 0 := by
intro this
rw [this, zero_mul] at hg1
cases hg1
have hg3 : g.natDegree < N.succ := by
rw [← mul_one g.natDegree, ← hg1]
exact Nat.mul_lt_mul_of_pos_left hp.one_lt hg2.bot_lt
rcases ih _ hg3 hg rfl with ⟨n, g, hg4, rfl⟩
refine ⟨n + 1, g, hg4, ?_⟩
rw [← hgf, expand_expand, pow_succ']
