English
The natSepDegree of the minimal polynomial is preserved under the expansion by q^n in ExpChar F q.
Русский
Разделяемая степень минимального многочлена сохраняется под расширением на q^n в ExpChar F q.
LaTeX
$$$ (minpoly F x).natSepDegree = 1 \Rightarrow \exists n\, y \ (minpoly F x = \expand F (q^n) (X - C y)) $$$
Lean4
/-- A monic polynomial over a field `F` of exponential characteristic `q` has separable degree one
if and only if it is of the form `(X ^ (q ^ n) - C y) ^ m` for some non-zero natural number `m`,
some natural number `n`, and some element `y` of `F`. -/
theorem natSepDegree_eq_one_iff (q : ℕ) [ExpChar F q] (hm : f.Monic) :
f.natSepDegree = 1 ↔ ∃ (m n : ℕ) (y : F), m ≠ 0 ∧ f = (X ^ q ^ n - C y) ^ m :=
by
refine ⟨fun h ↦ ?_, fun ⟨m, n, y, hm, h⟩ ↦ ?_⟩
· obtain ⟨m, n, y, hm, -, h⟩ := hm.eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one q h
exact ⟨m, n, y, hm, h⟩
simp_rw [h, natSepDegree_pow, hm, ite_false, natSepDegree_X_pow_char_pow_sub_C]
