finrank_eq_card_chooseBasisIndex — Mathlib

English

The finrank of a finite module M equals the cardinality of ChooseBasisIndex R M.

Русский

Финранк модуля M равен мощностям ChooseBasisIndex R M.

LaTeX

$$$\\mathrm{finrank}_R M = \\mathrm{Fintype.card}(\\mathrm{ChooseBasisIndex}\\, R\, M)$$$

Lean4

/-- The `finrank` of a free module `M` over `R` is the cardinality of `ChooseBasisIndex R M`. -/
theorem _root_.Module.finrank_eq_card_chooseBasisIndex [Module.Finite R M] :
    finrank R M = Fintype.card (ChooseBasisIndex R M) := by simp [finrank, rank_eq_card_chooseBasisIndex]

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