mathlib3 documentation

algebra.ne_zero

ne_zero typeclass #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main declarations #

source
@[class]
structure ne_zero {R : Type u_1} [has_zero R] (n : R) :
Prop
  • out : n ≠ 0

A type-class version of n ≠ 0.

Instances of this typeclass
source
theorem ne_zero.ne {R : Type u_1} [has_zero R] (n : R) [h : ne_zero n] :
n ≠ 0
source
theorem ne_zero.ne' {R : Type u_1} [has_zero R] (n : R) [h : ne_zero n] :
0 ≠ n
source
theorem ne_zero_iff {R : Type u_1} [has_zero R] {n : R} :
ne_zero n ↔ n ≠ 0
source
theorem not_ne_zero {R : Type u_1} [has_zero R] {n : R} :
¬ne_zero n ↔ n = 0
source
theorem eq_zero_or_ne_zero {α : Type u_1} [has_zero α] (a : α) :
a = 0 ∨ ne_zero a
source
@[simp]
theorem zero_ne_one {α : Type u_1} [has_zero α] [has_one α] [ne_zero 1] :
0 ≠ 1
source
@[simp]
theorem one_ne_zero {α : Type u_1} [has_zero α] [has_one α] [ne_zero 1] :
1 ≠ 0
source
theorem two_ne_zero {α : Type u_1} [has_zero α] [has_one α] [has_add α] [ne_zero 2] :
2 ≠ 0
source
theorem three_ne_zero {α : Type u_1} [has_zero α] [has_one α] [has_add α] [ne_zero 3] :
3 ≠ 0
source
theorem four_ne_zero {α : Type u_1} [has_zero α] [has_one α] [has_add α] [ne_zero 4] :
4 ≠ 0
source
theorem ne_zero_of_eq_one {α : Type u_1} [has_zero α] [has_one α] [ne_zero 1] {a : α} (h : a = 1) :
a ≠ 0
source
theorem zero_ne_one' (α : Type u_1) [has_zero α] [has_one α] [ne_zero 1] :
0 ≠ 1
source
theorem one_ne_zero' (α : Type u_1) [has_zero α] [has_one α] [ne_zero 1] :
1 ≠ 0
source
theorem two_ne_zero' (α : Type u_1) [has_zero α] [has_one α] [has_add α] [ne_zero 2] :
2 ≠ 0
source
theorem three_ne_zero' (α : Type u_1) [has_zero α] [has_one α] [has_add α] [ne_zero 3] :
3 ≠ 0
source
theorem four_ne_zero' (α : Type u_1) [has_zero α] [has_one α] [has_add α] [ne_zero 4] :
4 ≠ 0
source
@[protected, instance]
def ne_zero.succ {n : ℕ} :
ne_zero (n + 1)
source
theorem ne_zero.of_pos {M : Type u_3} {x : M} [preorder M] [has_zero M] (h : 0 < x) :
ne_zero x
source
@[protected, instance]
def ne_zero.coe_trans {R : Type u_1} {S : Type u_2} {M : Type u_3} {r : R} [has_zero M] [has_coe R S] [has_coe_t S M] [h : ne_zero ↑r] :
ne_zero ↑↑r
source
theorem ne_zero.trans {R : Type u_1} {S : Type u_2} {M : Type u_3} {r : R} [has_zero M] [has_coe R S] [has_coe_t S M] (h : ne_zero ↑↑r) :
ne_zero ↑r