ofMul_prod — Mathlib

English

For a Multiset S in a commutative monoid, the additive image of the product equals the sum of the additive images: ofMul S.prod = (S.map ofMul).sum.

Русский

Для мультсета S в коммутативном моноиде образ от произведения через ofMul равен сумме образов через ofMul.

LaTeX

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

Lean4

@[simp]
theorem ofMul_prod (s : Finset ι) (f : ι → M) : ofMul (∏ i ∈ s, f i) = ∑ i ∈ s, ofMul (f i) :=
  rfl

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