ofAdd_multiset_prod — Mathlib

English

For a Multiset S with Additive structure, the additive image of the sum equals the product of the additive images: ofAdd s.sum = (s.map ofAdd).prod.

Русский

Образ от суммы мультсета через ofAdd равен произведению образов через ofAdd.

LaTeX

$$$\operatorname{ofAdd}\left(\mathrm{sum}\,S\right) = \left(\mathrm{map}\ \operatorname{ofAdd} S\right).prod$$$

Lean4

@[simp]
theorem ofAdd_multiset_prod (s : Multiset M) : ofAdd s.sum = (s.map ofAdd).prod := by simp [ofAdd]; rfl

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