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 #

@[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
theorem ne_zero.ne {R : Type u_1} [has_zero R] (n : R) [h : ne_zero n] :
n 0
theorem ne_zero.ne' (n : ) (R : Type u_1) [has_zero R] [has_one R] [has_add R] [h : ne_zero n] :
n 0
theorem ne_zero_iff {R : Type u_1} [has_zero R] {n : R} :
theorem not_ne_zero {R : Type u_1} [has_zero R] {n : R} :
@[protected, instance]
def ne_zero.pnat {a : ℕ+} :
@[protected, instance]
def ne_zero.succ {n : } :
ne_zero (n + 1)
theorem ne_zero.of_pos {M : Type u_3} {x : M} [preorder M] [has_zero M] (h : 0 < x) :
theorem ne_zero.of_gt {M : Type u_3} {x y : M} [canonically_ordered_add_monoid M] (h : x < y) :
@[protected, instance]
def ne_zero.char_zero {M : Type u_3} {n : } [ne_zero n] [add_monoid M] [has_one M] [char_zero M] :
@[protected, instance]
def ne_zero.invertible {M : Type u_3} {x : M} [mul_zero_one_class M] [nontrivial M] [invertible x] :
@[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] :
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) :
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)] :
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) :
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) :
theorem ne_zero.pos {R : Type u_1} (r : R) [canonically_ordered_add_monoid R] [ne_zero r] :
0 < r
theorem ne_zero.of_not_dvd (M : Type u_3) {n p : } [add_monoid M] [has_one M] [char_p M p] (h : ¬p n) :
theorem ne_zero.of_no_zero_smul_divisors (R : Type u_1) (M : Type u_3) (n : ) [comm_ring R] [ne_zero n] [ring M] [nontrivial M] [algebra R M] [no_zero_smul_divisors R M] :
theorem ne_zero.of_ne_zero_coe (R : Type u_1) {n : } [has_zero R] [has_one R] [has_add R] [h : ne_zero n] :
theorem ne_zero.not_char_dvd (R : Type u_1) [add_monoid R] [has_one R] (p : ) [char_p R p] (k : ) [h : ne_zero k] :
¬p k
theorem ne_zero.pos_of_ne_zero_coe (R : Type u_1) {n : } [has_zero R] [has_one R] [has_add R] [ne_zero n] :
0 < n
theorem eq_zero_or_ne_zero {α : Type u_1} [has_zero α] (a : α) :
a = 0 ne_zero a