Theorems · Theorem · general algebraic systems

DFinsupp.single_eq_of_ne

∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] {i i' : ι} {b : β i},
  i' ≠ i → (fun₀ | i => b) i' = 0

Defined in

Mathlib.Data.DFinsupp.Defs

Cited by

12 results in Mathlib

Foundations

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

Assumes

ZeroDecidableEq