# 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) :

A type-class version of n ≠ 0.

• out : n 0

The proposition that n is not zero.

Instances
theorem NeZero.out {R : Type u_1} [Zero R] {n : R} [self : ] :
n 0

The proposition that n is not zero.

theorem NeZero.ne {R : Type u_1} [Zero R] (n : R) [h : ] :
n 0
theorem NeZero.ne' {R : Type u_1} [Zero R] (n : R) [h : ] :
0 n
theorem neZero_iff {R : Type u_1} [Zero R] {n : R} :
n 0
@[simp]
theorem neZero_zero_iff_false {α : Type u_2} [Zero α] :
theorem not_neZero {R : Type u_1} [Zero R] {n : R} :
¬ n = 0
theorem eq_zero_or_neZero {R : Type u_1} [Zero R] (a : R) :
a = 0
@[simp]
theorem zero_ne_one {α : Type u_2} [Zero α] [One α] [] :
0 1
@[simp]
theorem one_ne_zero {α : Type u_2} [Zero α] [One α] [] :
1 0
theorem ne_zero_of_eq_one {α : Type u_2} [Zero α] [One α] [] {a : α} (h : a = 1) :
a 0
theorem two_ne_zero {α : Type u_2} [Zero α] [OfNat α 2] [] :
2 0
theorem three_ne_zero {α : Type u_2} [Zero α] [OfNat α 3] [] :
3 0
theorem four_ne_zero {α : Type u_2} [Zero α] [OfNat α 4] [] :
4 0
theorem zero_ne_one' (α : Type u_2) [Zero α] [One α] [] :
0 1
theorem one_ne_zero' (α : Type u_2) [Zero α] [One α] [] :
1 0
theorem two_ne_zero' (α : Type u_2) [Zero α] [OfNat α 2] [] :
2 0
theorem three_ne_zero' (α : Type u_2) [Zero α] [OfNat α 3] [] :
3 0
theorem four_ne_zero' (α : Type u_2) [Zero α] [OfNat α 4] [] :
4 0
instance NeZero.succ {n : } :
NeZero (n + 1)
Equations
• =
theorem NeZero.of_pos {M : Type u_2} {x : M} [] [Zero M] (h : 0 < x) :
theorem Nat.pos_of_neZero (n : ) [] :
0 < n