English
If a monic polynomial f has natSepDegree 1 and splits over F, then f factors as (X − C y)^m with m > 0.
Русский
Если монный f имеет natSepDegree = 1 и распадается над F, тогда f = (X − C y)^m с m>0.
LaTeX
$$$ \exists m\,\exists y\ (m \neq 0 \land f = (X - C y)^m)$$$
Lean4
/-- If a monic irreducible polynomial over a field `F` of exponential characteristic `q` has
separable degree one, then it is of the form `X ^ (q ^ n) - C y` for some natural number `n`,
and some element `y` of `F`, such that either `n = 0` or `y` has no `q`-th root in `F`. -/
theorem eq_X_pow_char_pow_sub_C_of_natSepDegree_eq_one_of_irreducible (q : ℕ) [ExpChar F q] (hm : f.Monic)
(hi : Irreducible f) (h : f.natSepDegree = 1) :
∃ (n : ℕ) (y : F), (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = X ^ q ^ n - C y :=
by
obtain ⟨n, y, hf⟩ := (hm.natSepDegree_eq_one_iff_of_irreducible q hi).1 h
cases id ‹ExpChar F q› with
| zero =>
simp_rw [one_pow, pow_one] at hf ⊢
exact ⟨0, y, .inl rfl, hf⟩
| prime hq =>
refine ⟨n, y, (em _).imp id fun hn ⟨z, hy⟩ ↦ ?_, hf⟩
haveI := expChar_of_injective_ringHom (R := F) C_injective q
rw [hf, ← Nat.succ_pred hn, pow_succ, pow_mul, ← hy, frobenius_def, map_pow, ← sub_pow_expChar] at hi
exact not_irreducible_pow hq.ne_one hi
