English
For any index set ι, the length of the free finsupp module ι ⇝ M is ENat.card ι times the length of M: length_R(ι →_0 M) = ENat.card ι · length_R(M).
Русский
Для множества индексов ι длина модуля ι ⇝ M равна ENat.card(ι) умножить на длину M: length_R(ι →_0 M) = ENat.card(ι) · length_R(M).
LaTeX
$$$\operatorname{length}_R(\iota \to_0 M) = \operatorname{ENat.card}(\iota) \cdot \operatorname{length}_R(M)$$$
Lean4
@[simp]
theorem length_finsupp {ι : Type*} : Module.length R (ι →₀ M) = ENat.card ι * Module.length R M :=
by
cases finite_or_infinite ι
· cases nonempty_fintype ι
simp [(Finsupp.linearEquivFunOnFinite R M ι).length_eq]
nontriviality M
rw [ENat.card_eq_top_of_infinite, ENat.top_mul length_pos.ne', ENat.eq_top_iff_forall_ge]
intro m
obtain ⟨s, hs⟩ := Infinite.exists_subset_card_eq ι m
have : length R (s →₀ M) = ↑m * length R M := by simp [(Finsupp.linearEquivFunOnFinite R M _).length_eq, hs]
refine
le_trans ?_
(Module.length_le_of_injective (Finsupp.lmapDomain M R ((↑) : s → ι))
(Finsupp.mapDomain_injective Subtype.val_injective))
rw [this]
exact ENat.self_le_mul_right _ length_pos.ne'
