card_fixingSubgroup_eq_finrank — Mathlib

English

For a finite dimensional K⊂E over F, the cardinality of fixingSubgroup(K) equals the finrank of K over E.

Русский

Для конечномерного расширения K⊆E над F кардинал fixingSubgroup(K) равен finrank(K/E).

LaTeX

$$$\mathrm{card}(\operatorname{fixingSubgroup}(K)) = \mathrm{finrank}_E(K)$$$

Lean4

theorem card_fixingSubgroup_eq_finrank [FiniteDimensional F E] [IsGalois F E] :
    Nat.card (IntermediateField.fixingSubgroup K) = finrank K E := by
  conv_rhs => rw [← fixedField_fixingSubgroup K, IntermediateField.finrank_fixedField_eq_card]

Похожие утверждения