Theorems · Theorem · ring theory

Finsupp.onFinset_sum

∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] {s : Finset α} {f : α → M}
  {g : α → M → N} (hf : ∀ (a : α), f a ≠ 0 → a ∈ s),
  (∀ (a : α), g a 0 = 0) → (Finsupp.onFinset s f hf).sum g = ∑ a ∈ s, g a (f a)

If g maps a second argument of 0 to 0, summing it over the result of onFinset is the same as summing it over the original Finset.

Defined in

Mathlib.Algebra.BigOperators.Finsupp.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

ZeroAddCommMonoid