mk_eq_rank — Mathlib

English

For any basis v: ι → M, the cardinal lifted rank of ι equals the lifted rank of M, i.e., |ι|^ = rank_R(M)^{}.

Русский

Для любого базиса v: ι → M кардинальная величина ι равна рангу модуля M (с учётом подстановок по вселенным).

LaTeX

$$\\lvert \\iota \\rvert^{ } = \\operatorname{rank}_R(M)$$

Lean4

theorem mk_eq_rank (v : Basis ι R M) : Cardinal.lift.{v} #ι = Cardinal.lift.{w} (Module.rank R M) :=
  by
  haveI := nontrivial_of_invariantBasisNumber R
  rw [← v.mk_range_eq_rank, Cardinal.mk_range_eq_of_injective v.injective]

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