Big operators for finsupps
This file contains theorems relevant to big operators in finitely supported functions.
theorem
finset.sum_apply'
{α : Type u}
{ι : Type v}
{β : Type w}
[add_comm_monoid β]
{s : finset α}
{f : α → ι →₀ β}
(i : ι) :
theorem
finsupp.sum_apply'
{ι : Type v}
{β : Type w}
[add_comm_monoid β]
{γ : Type u₁}
{δ : Type v₁}
[add_comm_monoid δ]
(g : ι →₀ β)
(k : ι → β → γ → δ)
(x : γ) :
theorem
finsupp.sum_sum_index'
{α : Type u}
{ι : Type v}
{β : Type w}
[add_comm_monoid β]
{s : finset α}
{f : α → ι →₀ β}
{ε : Type w₁}
[add_comm_monoid ε]
{t : ι → β → ε}
(h0 : ∀ (i : ι), t i 0 = 0)
(h1 : ∀ (i : ι) (x y : β), t i (x + y) = t i x + t i y) :