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_2} [Zero α] : NeZero 0 ↔ False

theorem not_neZero {R : Type u_1} [Zero R] {n : R} : ¬NeZero n ↔ n = 0

theorem eq_zero_or_neZero {R : Type u_1} [Zero R] (a : R) : a = 0 ∨ NeZero a

@[simp]

theorem zero_ne_one {α : Type u_2} [Zero α] [One α] [NeZero 1] : 0 ≠ 1

@[simp]

theorem one_ne_zero {α : Type u_2} [Zero α] [One α] [NeZero 1] : 1 ≠ 0

theorem ne_zero_of_eq_one {α : Type u_2} [Zero α] [One α] [NeZero 1] {a : α} (h : a = 1) : a ≠ 0

theorem two_ne_zero {α : Type u_2} [Zero α] [OfNat α 2] [NeZero 2] : 2 ≠ 0

theorem three_ne_zero {α : Type u_2} [Zero α] [OfNat α 3] [NeZero 3] : 3 ≠ 0

theorem four_ne_zero {α : Type u_2} [Zero α] [OfNat α 4] [NeZero 4] : 4 ≠ 0

theorem zero_ne_one' (α : Type u_2) [Zero α] [One α] [NeZero 1] : 0 ≠ 1

theorem one_ne_zero' (α : Type u_2) [Zero α] [One α] [NeZero 1] : 1 ≠ 0

theorem two_ne_zero' (α : Type u_2) [Zero α] [OfNat α 2] [NeZero 2] : 2 ≠ 0

theorem three_ne_zero' (α : Type u_2) [Zero α] [OfNat α 3] [NeZero 3] : 3 ≠ 0

theorem four_ne_zero' (α : Type u_2) [Zero α] [OfNat α 4] [NeZero 4] : 4 ≠ 0

instance NeZero.succ {n : ℕ} : NeZero (n + 1)

Equations

• ⋯ = ⋯

theorem NeZero.of_pos {M : Type u_2} {x : M} [Preorder M] [Zero M] (h : 0 < x) : NeZero x