Theorems · Theorem · general algebraic systems

Finsupp.mapDomain_of_not_mem_image_support

∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α → β} {x : α →₀ M} {b : β},
  b ∉ f '' ↑x.support → (Finsupp.mapDomain f x) b = 0

Defined in

Mathlib.Data.Finsupp.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommMonoid