Documentation

Mathlib.Algebra.NeZero

NeZero typeclass #

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

Main declarations #

class NeZero {R : Type u_1} [inst : Zero R] (n : R) :
  • The proposition that n is not zero.

    out : n 0

A type-class version of n ≠ 0≠ 0.

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