toAdd_list_sum — Mathlib

English

For a List s of elements in Multiplicative M, the product over the list, mapped by toAdd, equals the sum of the toAdd of the elements: s.map toAdd .prod = toAdd (List.sum s).

Русский

Для списка элементов в Multiplicative M произведение списка, отображённое через toAdd, равно сумме образов элементов через toAdd.

LaTeX

$$$\left(\text{List}.sum s\right)^{\mathrm{toAdd}} = \left(\text{List}.prod (\text{toAdd} \circ s)\right)$$$

Lean4

@[simp]
theorem toAdd_list_sum (s : List (Multiplicative M)) : s.prod.toAdd = (s.map toAdd).sum := by simp [toAdd, ofAdd]; rfl

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