English
The fixed-point subfield is a normal extension of F; equivalently, for every element x in FixedPoints.subfield G F, its minimal polynomial over F splits in FixedPoints.subfield G F, and x is algebraic over F.
Русский
Подполе фиксированных точек является нормальным расширением F; для каждого элемента x из FixedPoints.subfield G F минимальный полином над F разложим в FixedPoints.subfield G F, и x алгебраически над F.
LaTeX
$$$\\text{Normal}( \\operatorname{FixedPoints.subfield } G F, F)$$$
Lean4
instance normal : Normal (FixedPoints.subfield G F) F
where
isAlgebraic x := (isIntegral G F x).isAlgebraic
splits'
x :=
(Polynomial.splits_id_iff_splits _).1 <| by
cases nonempty_fintype G
rw [← minpoly_eq_minpoly, minpoly, coe_algebraMap, ← Subfield.toSubring_subtype_eq_subtype,
Polynomial.map_toSubring _ (subfield G F).toSubring, prodXSubSMul]
exact Polynomial.splits_prod _ fun _ _ => Polynomial.splits_X_sub_C _
