NeZero typeclass

We create a typeclass NeZero n which carries around the fact that (n : R) ≠ 0.

Main declarations

• NeZero: n ≠ 0 as a typeclass.

class NeZero {R : Type u_1} [Zero R] (n : R) : Prop

A type-class version of n ≠ 0.

• out : n ≠ 0

  The proposition that n is not zero.

theorem NeZero.ne {R : Type u_1} [Zero R] (n : R) [h : NeZero n] : n ≠ 0

theorem NeZero.ne' {R : Type u_1} [Zero R] (n : R) [h : NeZero n] : 0 ≠ n

theorem neZero_iff {R : Type u_1} [Zero R] {n : R} : NeZero n ↔ n ≠ 0

@[simp]

theorem neZero_zero_iff_false {α : Type u_1} [Zero α] : NeZero 0 ↔ False

instance instNeZeroNatIte {p : Prop} [Decidable p] {n m : Nat} [NeZero n] [NeZero m] : NeZero (if p then n else m)

instance instNeZeroNatHAdd {n m : Nat} [h : NeZero n] : NeZero (n + m)

instance instNeZeroNatHAdd_1 {n m : Nat} [h : NeZero m] : NeZero (n + m)

instance instNeZeroNatHMul {n m : Nat} [hn : NeZero n] [hm : NeZero m] : NeZero (n * m)