Theorems · Theorem · general algebraic systems

DFinsupp.extendWith_single_zero

∀ {ι : Type u} {α : Option ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : Option ι) → Zero (α i)] (i : ι)
  (x : α (some i)), (DFinsupp.extendWith 0 fun₀ | i => x) = fun₀ | some i => x

Defined in

Mathlib.Data.DFinsupp.Defs

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqZero