toAdd_prod — Mathlib

English

For a Finset s and a function f: ι → Multiplicative M, the product over s mapped by toAdd equals the sum of the toAdd of the elements: (s.prod f).toAdd = ∑ i ∈ s, (f i).toAdd.

Русский

Произведение по Finset, отображённое через toAdd, равно сумме образов через toAdd элементов.

LaTeX

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

Lean4

@[simp]
theorem toAdd_prod (s : Finset ι) (f : ι → Multiplicative M) : (∏ i ∈ s, f i).toAdd = ∑ i ∈ s, (f i).toAdd :=
  rfl

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