finset_sum_apply — Mathlib

English

For a Finset S, and sum of finsupps f i, the value at an argument equals the sum of their values: (∑ i∈S, f i) a = ∑ i∈S, f i a.

Русский

Для множества S и суммы f_i, значение в точке равно сумме значений: (∑ i∈S, f_i) a = ∑ i∈S, f_i a.

LaTeX

$$$$ \\Big( \\sum_{i \\in S} f_i \\Big) a = \\sum_{i \\in S} (f_i a) $$$$

Lean4

theorem finset_sum_apply [AddCommMonoid N] (S : Finset ι) (f : ι → α →₀ N) (a : α) :
    (∑ i ∈ S, f i) a = ∑ i ∈ S, f i a :=
  map_sum (applyAddHom a) _ _

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