Big operators for finsupps #
This file contains theorems relevant to big operators in finitely supported functions.
theorem
finset.sum_apply'
{α : Type u_1}
{ι : Type u_2}
{A : Type u_4}
[add_comm_monoid A]
{s : finset α}
{f : α → ι →₀ A}
(i : ι) :
theorem
finsupp.sum_apply'
{ι : Type u_2}
{γ : Type u_3}
{A : Type u_4}
{B : Type u_5}
[add_comm_monoid A]
[add_comm_monoid B]
(g : ι →₀ A)
(k : ι → A → γ → B)
(x : γ) :
theorem
finsupp.sum_sum_index'
{α : Type u_1}
{ι : Type u_2}
{A : Type u_4}
{C : Type u_6}
[add_comm_monoid A]
[add_comm_monoid C]
{t : ι → A → C}
(h0 : ∀ (i : ι), t i 0 = 0)
(h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y)
{s : finset α}
{f : α → ι →₀ A} :
theorem
finsupp.sum_mul
{α : Type u_1}
{R : Type u_7}
{S : Type u_8}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
(b : S)
(s : α →₀ R)
{f : α → R → S} :
theorem
finsupp.mul_sum
{α : Type u_1}
{R : Type u_7}
{S : Type u_8}
[non_unital_non_assoc_semiring R]
[non_unital_non_assoc_semiring S]
(b : S)
(s : α →₀ R)
{f : α → R → S} :