rank_eq_card_chooseBasisIndex — Mathlib

English

The rank of a free module M over R equals the cardinality of ChooseBasisIndex R M.

Русский

Ранг свободного модуля M над R равен кардинальности ChooseBasisIndex R M.

LaTeX

$$$\\operatorname{rank}_R M = \\#(\\mathrm{ChooseBasisIndex}\\, R\, M)$$$

Lean4

/-- The rank of a free module `M` over `R` is the cardinality of `ChooseBasisIndex R M`. -/
theorem rank_eq_card_chooseBasisIndex : Module.rank R M = #(ChooseBasisIndex R M) :=
  (chooseBasis R M).mk_eq_rank''.symm

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