English
For a Galois group G of L/K, the cardinality of G equals the dimension of L as a K-vector space.
Русский
Для Галуа-группы G над L/K кардиналилитет G равен размерности пространства L над K.
LaTeX
$$$|G| = \\dim_K L$$$
Lean4
theorem card_eq_finrank [IsGaloisGroup G K L] : Nat.card G = Module.finrank K L :=
by
rcases fintypeOrInfinite G with _ | hG
· have : FaithfulSMul G L := faithful K
rw [← IntermediateField.finrank_bot', ← fixedPoints_eq_bot G, Nat.card_eq_fintype_card]
exact (FixedPoints.finrank_eq_card G L).symm
· rw [Nat.card_eq_zero_of_infinite, eq_comm]
contrapose! hG
have : FiniteDimensional K L := FiniteDimensional.of_finrank_pos (Nat.zero_lt_of_ne_zero hG)
exact
Finite.of_injective (MulSemiringAction.toAlgAut G K L)
(fun _ _ ↦ (faithful K).eq_of_smul_eq_smul ∘ DFunLike.ext_iff.mp)
