Theorems · Theorem · ring theory

Finsupp.sum_finsetSum_index

∀ {α : Type u_1} {ι : Type u_2} {M : Type u_8} {N : Type u_10} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  {s : Finset ι} {g : ι → α →₀ M} {h : α → M → N},
  (∀ (a : α), h a 0 = 0) →
    (∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) → ∑ i ∈ s, (g i).sum h = (∑ i ∈ s, g i).sum h

Defined in

Mathlib.Algebra.BigOperators.Finsupp.Basic

Cited by

3 results in Mathlib

Foundations

Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidAddCommMonoid