A sign that is zero after its cast

A candidate for Mathlib.Basic.Sign.Defs: the cast of a sign into a type in which 1 ≠ 0, such as ℤ, is 0 only for the sign 0 (SignType.coe_eq_zero), so that with sign_eq_zero_iff the integer sign of a is 0 exactly for a = 0.

Main statements

• SignType.coe_eq_zero: the cast of a sign is 0 only for the sign 0.

@[simp]

theorem SignType.coe_eq_zero {α : Type u_1} [One α] [SubtractionMonoid α] [NeZero 1] {s : SignType} : ↑s = 0 ↔ s = 0