Theorems · Theorem · general algebraic systems

Finsupp.mapDomain_sum

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

Defined in

Mathlib.Data.Finsupp.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommMonoidZero