finrank_eq_rank — Mathlib

English

Let R be a semiring and M an additive commutative monoid with a module structure over R. If M is finite as an R-module, then the natural finrank of M, when viewed as a cardinal, equals the rank of M over R.

Русский

Пусть R — полугруппа, M — аддитивная коммутативная моноида с модулем над R. Если M является конечномерным R-модулем, то натуральная размерность finrank R M, приводимая к кардиналу, равна рангу M над R.

LaTeX

$$$\\uparrow(\\operatorname{finrank} R M) = \\operatorname{Module.rank} R M$$$

Lean4

/-- If `M` is finite, `finrank M = rank M`. -/
@[simp]
theorem finrank_eq_rank [Module.Finite R M] : ↑(finrank R M) = Module.rank R M := by
  rw [Module.finrank, cast_toNat_of_lt_aleph0 (rank_lt_aleph0 R M)]

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