ofAdd_sum — Mathlib

English

For a Finite set s and a function f: ι → M, the additive image of the sum equals the product of the additive images: ofAdd (∑ i ∈ s, f i) = ∏ i ∈ s, ofAdd (f i).

Русский

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

LaTeX

$$$\operatorname{ofAdd}\left(\sum i \in s, f(i)\right) = \prod i \in s, \operatorname{ofAdd}(f(i))$$$

Lean4

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

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