finrank_eq_card_basis — Mathlib

English

If M has a finite basis, then the rank of M equals the cardinality of the basis: rank_R(M) = card ι.

Русский

Если у M есть конечный базис, то ранг M равен кардиналу ι.

LaTeX

$$\\operatorname{rank}_R(M) = |\\iota|$$

Lean4

/-- If a vector space (or module) has a finite basis, then its dimension (or rank) is equal to the
cardinality of the basis. -/
theorem finrank_eq_card_basis {ι : Type w} [Fintype ι] (h : Basis ι R M) : finrank R M = Fintype.card ι :=
  finrank_eq_of_rank_eq (rank_eq_card_basis h)

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