Documentation

Mathlib.Algebra.NeZero

NeZero typeclass #

We give basic facts about the NeZero n typeclass.

theorem not_neZero {R : Type u_1} [Zero R] {n : R} :
theorem eq_zero_or_neZero {R : Type u_1} [Zero R] (a : R) :
@[simp]
theorem zero_ne_one {α : Type u_2} [Zero α] [One α] [NeZero 1] :
@[simp]
theorem one_ne_zero {α : Type u_2} [Zero α] [One α] [NeZero 1] :
theorem ne_zero_of_eq_one {α : Type u_2} [Zero α] [One α] [NeZero 1] {a : α} (h : a = 1) :
theorem two_ne_zero {α : Type u_2} [Zero α] [OfNat α 2] [NeZero 2] :
theorem three_ne_zero {α : Type u_2} [Zero α] [OfNat α 3] [NeZero 3] :
theorem four_ne_zero {α : Type u_2} [Zero α] [OfNat α 4] [NeZero 4] :
theorem zero_ne_one' (α : Type u_2) [Zero α] [One α] [NeZero 1] :
theorem one_ne_zero' (α : Type u_2) [Zero α] [One α] [NeZero 1] :
theorem two_ne_zero' (α : Type u_2) [Zero α] [OfNat α 2] [NeZero 2] :
theorem three_ne_zero' (α : Type u_2) [Zero α] [OfNat α 3] [NeZero 3] :
theorem four_ne_zero' (α : Type u_2) [Zero α] [OfNat α 4] [NeZero 4] :
theorem NeZero.of_pos {M : Type u_2} {x : M} [Preorder M] [Zero M] (h : 0 < x) :