Theorems · Theorem · general algebraic systems

Finsupp.single_apply

∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a a' : α} {b : M} [inst_1 : Decidable (a = a')],
  (fun₀ | a => b) a' = if a = a' then b else 0

Defined in

Mathlib.Data.Finsupp.Single

Cited by

99 results in Mathlib

Foundations

Depth 60 from the axioms, rests on 837 definitions · uses propext, Classical.choice, Quot.sound

Assumes

ZeroDecidable