English
For x ≠ 0, the separable degree of C x · (X − C y)^n equals that of (X − C y)^n, i.e., 0 if n = 0, else 1.
Русский
При x ≠ 0, natSepDegree(C x · (X − C y)^n) равно natSepDegree((X − C y)^n), то есть 0 при n=0, иначе 1.
LaTeX
$$$ (C x \cdot (X - C y)^n).natSepDegree = \begin{cases}0, & n=0 \\\ 1, & n>0 \end{cases} $$$
Lean4
/-- A monic irreducible polynomial over a field `F` of exponential characteristic `q` has
separable degree one if and only if it is of the form `Polynomial.expand F (q ^ n) (X - C y)`
for some `n : ℕ` and `y : F`. -/
theorem natSepDegree_eq_one_iff_of_monic' (q : ℕ) [ExpChar F q] (hm : f.Monic) (hi : Irreducible f) :
f.natSepDegree = 1 ↔ ∃ (n : ℕ) (y : F), f = expand F (q ^ n) (X - C y) :=
by
refine ⟨fun h ↦ ?_, fun ⟨n, y, h⟩ ↦ ?_⟩
· obtain ⟨g, h1, n, rfl⟩ := hi.hasSeparableContraction q
have h2 : g.natDegree = 1 := by rwa [natSepDegree_expand _ q, h1.natSepDegree_eq_natDegree] at h
rw [((monic_expand_iff <| expChar_pow_pos F q n).mp hm).eq_X_add_C h2]
exact ⟨n, -(g.coeff 0), by rw [map_neg, sub_neg_eq_add]⟩
rw [h, natSepDegree_expand _ q, natSepDegree_X_sub_C]
