finrank_fixedField_eq_card — Mathlib

English

For finite-dimensional E over F and subgroup H of automorphisms, the finite rank of E over fixedField H equals the cardinality of H.

Русский

При конечной размерности E/F и подгруппе H автоморфизмов, finrank(E over fixedField H) = |H|.

LaTeX

$$finrank (fixedField H) E = Nat.card H$$

Lean4

theorem finrank_fixedField_eq_card [FiniteDimensional F E] : finrank (fixedField H) E = Nat.card H :=
  by
  have := Fintype.ofFinite H
  rw [Nat.card_eq_fintype_card]
  exact FixedPoints.finrank_eq_card H E

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