ofMul_list_prod — Mathlib

English

For any Monoid M, the additive image of the product of a list equals the sum of the additive images of the elements: ofMul (List.prod s) = List.sum (List.map ofMul s).

Русский

Для любого моноида M сумма добавления равна сумме образов элементов через ofMul: ofMul (список произведений) = сумма образов элементов.

LaTeX

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

Lean4

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

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