English
Equality of minpoly when moving to fixed-point subfield: minpoly G F x equals minpoly (subfield) x.
Русский
Минполином x над G F совпадает с минполином x над подполем фиксированных точек.
LaTeX
$$$\\minpoly G F x = \\minpoly (FixedPoints.subfield G F) x$$$
Lean4
/-- Let $F$ be a field. Let $G$ be a finite group acting faithfully on $F$.
Then $[F : F^G] = |G|$. -/
@[stacks 09I3 "second part"]
theorem finrank_eq_card [Fintype G] [FaithfulSMul G F] : finrank (FixedPoints.subfield G F) F = Fintype.card G :=
le_antisymm (FixedPoints.finrank_le_card G F) <|
calc
Fintype.card G ≤ Fintype.card (F →ₐ[FixedPoints.subfield G F] F) :=
Fintype.card_le_of_injective _ (MulSemiringAction.toAlgHom_injective _ F)
_ ≤ finrank F (F →ₗ[FixedPoints.subfield G F] F) := (finrank_algHom (subfield G F) F)
_ = finrank (FixedPoints.subfield G F) F := finrank_linearMap_self _ _ _
