Documentation

Mathlib.Algebra.NeZero

NeZero typeclass #

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

Main declarations #

source
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.

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