Theorems · Theorem · general algebraic systems

Finsupp.equivMapDomain_single

∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α ≃ β) (a : α) (b : M),
  (Finsupp.equivMapDomain f fun₀ | a => b) = fun₀ | f a => b

Defined in

Mathlib.Data.Finsupp.Basic

Cited by

11 results in Mathlib

Foundations

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

Assumes

Zero