English
For a fixed q with ExpChar F q, the natSepDegree of the minimal polynomial equals 1 if and only if it is of the form expand F (q^n) (X − C y).
Русский
При фиксированном q с ExpChar F q natSepDegree минимального полинома равна 1 тогда и только тогда, когда он имеет вид expand F (q^n) (X − C y).
LaTeX
$$$ (minpoly F x).natSepDegree = 1 \iff \exists n\, \exists y\ (minpoly F x = \expand F (q^n) (X - C y)) $$$
Lean4
/-- The minimal polynomial of an element of `E / F` of exponential characteristic `q` has
separable degree one if and only if the minimal polynomial is of the form
`Polynomial.expand F (q ^ n) (X - C y)` for some `n : ℕ` and `y : F`. -/
theorem natSepDegree_eq_one_iff_eq_expand_X_sub_C :
(minpoly F x).natSepDegree = 1 ↔ ∃ (n : ℕ) (y : F), minpoly F x = expand F (q ^ n) (X - C y) :=
by
refine ⟨fun h ↦ ?_, fun ⟨n, y, h⟩ ↦ ?_⟩
· have halg : IsIntegral F x := by_contra fun h' ↦ by simp only [eq_zero h', natSepDegree_zero, zero_ne_one] at h
exact (minpoly.irreducible halg).natSepDegree_eq_one_iff_of_monic' q (minpoly.monic halg) |>.1 h
rw [h, natSepDegree_expand _ q, natSepDegree_X_sub_C]
