mk_finrank_eq_card_basis — Mathlib

English

If M is finite, then the cardinality of any basis equals finrank_R(M), i.e., finrank_R(M) = card ι (as a cardinal).

Русский

Если модуль конечен, то кардинал любого базиса равен finrank_R(M).

LaTeX

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

Lean4

/-- If a free module is of finite rank, then the cardinality of any basis is equal to its
`finrank`. -/
theorem mk_finrank_eq_card_basis [Module.Finite R M] {ι : Type w} (h : Basis ι R M) :
    (finrank R M : Cardinal.{w}) = #ι :=
  by
  cases @nonempty_fintype _ (Module.Finite.finite_basis h)
  rw [Cardinal.mk_fintype, finrank_eq_card_basis h]

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