@[reducible, inline]

abbrev Cslib.DecidableEqZero (α : Type u_1) [Zero α] : Type u_1

Equality to Zero is decidable for all elements of a type (α).

Equations

• Cslib.DecidableEqZero α = ((a : α) → Decidable (a = 0))