English
Let ι be a finite index set and (M_i) be a family of R-modules. Then the length of the product Π_i M_i equals the sum of the lengths: length_R(Π_i M_i) = ∑_i length_R(M_i).
Русский
Пусть ι конечно; совокупность модулей (M_i). Тогда длина произведения Π_i M_i равна сумме длин: length_R(Π_i M_i) = ∑_i length_R(M_i).
LaTeX
$$$\operatorname{length}_R\left(\prod_{i} M_i\right) = \sum_{i} \operatorname{length}_R(M_i)$$$
Lean4
@[simp]
theorem length_pi_of_fintype :
∀ {ι : Type*} [Fintype ι] (M : ι → Type*) [∀ i, AddCommGroup (M i)] [∀ i, Module R (M i)],
Module.length R (Π i, M i) = ∑ i, Module.length R (M i) :=
by
apply Fintype.induction_empty_option
· intro α β _ e IH M _ _
let _ : Fintype α := .ofEquiv β e.symm
rw [← (LinearEquiv.piCongrLeft R M e).length_eq, IH, e.sum_comp (length R <| M ·)]
· intro M _ _
simp [Module.length_eq_zero]
· intro ι _ IH M _ _
rw [(LinearEquiv.piOptionEquivProd _).length_eq, Module.length_prod, IH, add_comm, Fintype.sum_option, add_comm]
