English
The fixed-point subfield extension has rank at most the size of G, i.e., dim_F of FixedPoints.subfield G F is ≤ |G|, under suitable finiteness assumptions.
Русский
Расширение фиксированных точек имеет ранг не превосходящий размер группы; то есть размерность фиксированного подполя над F не превосходит |G|.
LaTeX
$$$\\operatorname{rank}_F(\\operatorname{FixedPoints.subfield } G F) \\le |G|$$$
Lean4
theorem rank_le_card : Module.rank (FixedPoints.subfield G F) F ≤ Fintype.card G :=
rank_le fun s hs => by
simpa only [rank_fun', Cardinal.mk_coe_finset, Finset.coe_sort_coe, Cardinal.lift_natCast, Nat.cast_le] using
(linearIndependent_smul_of_linearIndependent G F hs).cardinal_lift_le_rank
