Theorems · Theorem · general algebraic systems

DFinsupp.single_apply

∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] {i i' : ι} {b : β i},
  (fun₀ | i => b) i' = if h : i = i' then Eq.recOn h b else 0

Defined in

Mathlib.Data.DFinsupp.Defs

Cited by

35 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Quot.sound

Assumes

ZeroDecidableEq