mathlib documentation

algebra.ne_zero

ne_zero typeclass #

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' (n : ℕ) (R : Type u_1) [add_monoid_with_one R] [h : ne_zero ↑n] :
↑n ≠ 0
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
@[protected, instance]
def ne_zero.pnat {a : ℕ+} :
ne_zero ↑a
source
@[protected, instance]
def ne_zero.succ {n : ℕ} :
ne_zero (n + 1)
source
@[protected, instance]
def ne_zero.one (R : Type u_1) [mul_zero_one_class R] [nontrivial R] :
ne_zero 1
source
theorem ne_zero.pos {R : Type u_1} (r : R) [canonically_ordered_add_monoid R] [ne_zero r] :
0 < r
source
theorem ne_zero.of_pos {M : Type u_3} {x : M} [preorder M] [has_zero M] (h : 0 < x) :
ne_zero x
source
theorem ne_zero.of_gt {M : Type u_3} {x y : M} [canonically_ordered_add_monoid M] (h : x < y) :
ne_zero y
source
@[protected, instance]
def ne_zero.of_gt' {M : Type u_3} {y : M} [canonically_ordered_add_monoid M] [has_one M] [fact (1 < y)] :
ne_zero y
source
@[protected, instance]
def ne_zero.bit0 {M : Type u_3} {x : M} [canonically_ordered_add_monoid M] [ne_zero x] :
ne_zero (bit0 x)
source
@[protected, instance]
def ne_zero.bit1 {M : Type u_3} {x : M} [canonically_ordered_comm_semiring M] [nontrivial M] :
ne_zero (bit1 x)
source
@[protected, instance]
def ne_zero.pow {M : Type u_3} {x : M} {n : ℕ} [monoid_with_zero M] [no_zero_divisors M] [ne_zero x] :
ne_zero (x ^ n)
source
@[protected, instance]
def ne_zero.mul {M : Type u_3} {x y : M} [has_zero M] [has_mul M] [no_zero_divisors M] [ne_zero x] [ne_zero y] :
ne_zero (x * y)
source
@[protected, instance]
def ne_zero.char_zero {M : Type u_3} {n : ℕ} [ne_zero n] [add_monoid_with_one M] [char_zero M] :
ne_zero ↑n
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
source
theorem ne_zero.of_map {R : Type u_1} {M : Type u_3} {F : Type u_4} {r : R} [has_zero R] [has_zero M] [zero_hom_class F R M] (f : F) [ne_zero (⇑f r)] :
ne_zero r
source
theorem ne_zero.nat_of_ne_zero {R : Type u_1} {S : Type u_2} {F : Type u_4} {n : ℕ} [semiring R] [semiring S] [ring_hom_class F R S] (f : F) [hn : ne_zero ↑n] :
ne_zero ↑n
source
theorem ne_zero.of_injective {R : Type u_1} {M : Type u_3} {F : Type u_4} {r : R} [has_zero R] [h : ne_zero r] [has_zero M] [zero_hom_class F R M] {f : F} (hf : function.injective ⇑f) :
ne_zero (⇑f r)
source
theorem ne_zero.nat_of_injective {R : Type u_1} {M : Type u_3} {F : Type u_4} {n : ℕ} [non_assoc_semiring M] [non_assoc_semiring R] [h : ne_zero ↑n] [ring_hom_class F R M] {f : F} (hf : function.injective ⇑f) :
ne_zero ↑n
source
theorem ne_zero.of_ne_zero_coe (R : Type u_1) {n : ℕ} [add_monoid_with_one R] [h : ne_zero ↑n] :
ne_zero n
source
theorem ne_zero.pos_of_ne_zero_coe (R : Type u_1) {n : ℕ} [add_monoid_with_one R] [ne_zero ↑n] :
0 < n