English
Let M be a free R-module. Then length_R(M) equals rank_R(M) converted to ENat times length_R(R).
Русский
Пусть M — свободный модуль над R. Тогда length_R(M) равна rank_R(M), приведённому к ENat, умноженному на length_R(R).
LaTeX
$$$\operatorname{length}_R(M) = (\operatorname{rank}_R M)^{\mathrm{toENat}} \cdot \operatorname{length}_R(R)$$$
Lean4
theorem length_of_free [Module.Free R M] : Module.length R M = (Module.rank R M).toENat * Module.length R R :=
by
let b := Module.Free.chooseBasis R M
nontriviality R
nontriviality M
by_cases H : Module.length R R = ⊤
· rw [b.repr.length_eq, Module.length_finsupp, H, ENat.mul_top', ENat.mul_top']
congr 1
simp [ENat.card_eq_zero_iff_empty, rank_pos_of_free.ne']
rw [← ne_eq, Module.length_ne_top_iff, isFiniteLength_iff_isNoetherian_isArtinian] at H
cases H
let b := Module.Free.chooseBasis R M
rw [b.repr.length_eq, Module.length_finsupp, Free.rank_eq_card_chooseBasisIndex, ENat.card]
