English
If M is a free R-module, then length_R(M) = rank_R(M).toENat × length_R(R).
Русский
Если M свободный модуль над R, то length_R(M) = rank_R(M).toENat × length_R(R).
LaTeX
$$$\operatorname{length}_R(M) = (\operatorname{rank}_R M)^{\mathrm{toENat}} \cdot \operatorname{length}_R(R)$$$
Lean4
@[simp]
theorem length_pi {ι : Type*} : Module.length R (ι → M) = ENat.card ι * Module.length R M :=
by
cases finite_or_infinite ι
· cases nonempty_fintype ι
simp
nontriviality M
rw [ENat.card_eq_top_of_infinite, ENat.top_mul length_pos.ne', ← top_le_iff]
refine le_trans ?_ (Module.length_le_of_injective Finsupp.lcoeFun DFunLike.coe_injective)
simp [ENat.top_mul length_pos.ne']
