Theorems · Theorem · ring theory

Finsupp.sum_embDomain

∀ {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] {v : α →₀ M}
  {f : α ↪ β} {g : β → M → N}, (Finsupp.embDomain f v).sum g = v.sum fun a b => g (f a) b

Defined in

Mathlib.Algebra.BigOperators.Finsupp.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

ZeroAddCommMonoid