English
In characteristic exponential q, expanding f by the q-power map does not change its separable degree.
Русский
В характеристике экспоненциального типа q расширение f по карте q не изменяет его разделяемую степень.
LaTeX
$$$ (\operatorname{expand} F (q^n) f).natSepDegree = f.natSepDegree $$$
Lean4
/-- If a field `F` is of exponential characteristic `q`, then `Polynomial.expand F (q ^ n) f`
and `f` have the same separable degree. -/
theorem natSepDegree_expand (q : ℕ) [hF : ExpChar F q] {n : ℕ} : (expand F (q ^ n) f).natSepDegree = f.natSepDegree :=
by
obtain - | hprime := hF
· simp only [one_pow, expand_one]
haveI := Fact.mk hprime
classical
simpa only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_def, map_expand, Fintype.card_coe] using
Fintype.card_eq.2 ⟨(f.map (algebraMap F (AlgebraicClosure F))).rootsExpandPowEquivRoots q n⟩
