toMul_sum — Mathlib

English

For a Finset s and a function f: ι → Additive M, the image under toMul of the finite sum equals the finite product of the toMul images: (∑ i ∈ s, f i).toMul = ∏ i ∈ s, (f i).toMul.

Русский

Для конечного множества s и функции f: ι → Additive M образ суммы toMul равен произведению образов toMul каждого элемента.

LaTeX

$$$\left(\sum i \in s, f(i)\right)^{\mathrm{toMul}} = \prod i \in s, (f(i))^{\mathrm{toMul}}$$$

Lean4

@[simp]
theorem toMul_sum (s : Finset ι) (f : ι → Additive M) : (∑ i ∈ s, f i).toMul = ∏ i ∈ s, (f i).toMul :=
  rfl

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