English
The fixed-point subfield extension is separable over F; i.e., FixedPoints.isSeparable asserts Algebra.IsSeparable (FixedPoints.subfield G F) F.
Русский
Расширение фиксированных точек над F развалимо на простые корни; то есть это разделимоe расширение.
LaTeX
$$$\\text{IsSeparable}(\\operatorname{FixedPoints.subfield } G F, F)$$$
Lean4
instance isSeparable : Algebra.IsSeparable (FixedPoints.subfield G F) F := by
classical
exact
⟨fun x => by
cases nonempty_fintype G
rw [IsSeparable, ← minpoly_eq_minpoly, ← Polynomial.separable_map (FixedPoints.subfield G F).subtype, minpoly, ←
Subfield.toSubring_subtype_eq_subtype, Polynomial.map_toSubring _ (subfield G F).toSubring]
exact Polynomial.separable_prod_X_sub_C_iff.2 (injective_ofQuotientStabilizer G x)⟩
