toMul_list_sum — Mathlib

English

For a list s of elements of Additive M, the image under toMul of the sum equals the product of the images under toMul: toMul (List.sum s) = List.prod (List.map toMul s).

Русский

Для списка элементов Additive M образ перемножения toMul от суммы равен произведению образов toMul от каждого элемента.

LaTeX

$$$\operatorname{toMul}\left(\sum x \in s, x\right) = \prod x \in s, \operatorname{toMul}(x)$$$

Lean4

@[simp]
theorem toMul_list_sum (s : List (Additive M)) : s.sum.toMul = (s.map toMul).prod := by simp [toMul, ofMul]; rfl

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