length_prod — Mathlib

English

For modules M and N over R, the length of the direct product M × N equals the sum of the lengths: length_R(M × N) = length_R(M) + length_R(N).

Русский

Для модулей M и N над R длина прямого произведения M × N равна сумме длин: length_R(M × N) = length_R(M) + length_R(N).

LaTeX

$$$\operatorname{length}_R(M \times N) = \operatorname{length}_R(M) + \operatorname{length}_R(N)$$$

Lean4

@[simp]
theorem length_prod : Module.length R (M × N) = Module.length R M + Module.length R N :=
  Module.length_eq_add_of_exact _ _ LinearMap.inl_injective LinearMap.snd_surjective .inl_snd

Похожие утверждения