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)]