Theorems · Theorem · general algebraic systems

Finsupp.sum_mapDomain_index

∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  {f : α → β} {s : α →₀ M} {h : β → M → N},
  (∀ (b : β), h b 0 = 0) →
    (∀ (b : β) (m₁ m₂ : M), h b (m₁ + m₂) = h b m₁ + h b m₂) →
      (Finsupp.mapDomain f s).sum h = s.sum fun a m => h (f a) m

Defined in

Mathlib.Data.Finsupp.Basic

Cited by

19 results in Mathlib

Foundations

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

Assumes

AddCommMonoidAddCommMonoid