Theorems · Definition · general algebraic systems

Finsupp.update

{α : Type u_1} → {M : Type u_5} → [inst : Zero M] → (α →₀ M) → α → M → α →₀ M

Replace the value of a α →₀ M at a given point a : α by a given value b : M. If b = 0, this amounts to removing a from the Finsupp.support. Otherwise, if a was not in the Finsupp.support, it is added to it. This is the finitely-supported version of Function.update.

Defined in

Mathlib.Data.Finsupp.Single

Cited by

52 results in Mathlib

Foundations

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

Assumes

Zero