Theorems · Theorem · field theory

FixedPoints.finrank_eq_card

∀ (G : Type u_2) (F : Type u_3) [inst : Group G] [inst_1 : Field F] [inst_2 : MulSemiringAction G F]
  [inst_3 : Fintype G] [FaithfulSMul G F], Module.finrank (↥(FixedPoints.subfield G F)) F = Fintype.card G

Let $F$ be a field. Let $G$ be a finite group acting faithfully on $F$. Then $[F : F^G] = |G|$.

Defined in

Mathlib.FieldTheory.Fixed

Cited by

3 results in Mathlib

Foundations

Depth 140 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupFieldMulSemiringActionFintypeFaithfulSMul