rank_eq_card_basis — Mathlib

English

If a finite basis v: ι → M exists, then rank_R(M) equals the cardinality of ι, i.e., rank_R(M) = |ι|.

Русский

Если существует конечный базис v: ι → M, то ранг модуля равен кардинальности ι: rank_R(M) = |ι|.

LaTeX

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

Lean4

/-- If a vector space has a finite basis, then its dimension (seen as a cardinal) is equal to the
cardinality of the basis. -/
theorem rank_eq_card_basis {ι : Type w} [Fintype ι] (h : Basis ι R M) : Module.rank R M = Fintype.card ι := by
  classical
  haveI := nontrivial_of_invariantBasisNumber R
  rw [← h.mk_range_eq_rank, Cardinal.mk_fintype, Set.card_range_of_injective h.injective]

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