NeZero typeclass

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

Main declarations

• NeZero: n ≠ 0 as a typeclass.

class NeZero {R : Type u_1} [Zero R] (n : R) : Prop

A type-class version of n ≠ 0.

• out : n ≠ 0

  The proposition that n is not zero.

Instances

• Fintype.instNeZeroNatCardOfNonempty
• Invertible.toNeZero
• Nat.AtLeastTwo.toNeZero
• Nat.instNeZeroHPow
• Nat.instNeZeroSucc
• NeZero.charZero
• NeZero.charZero_ofNat
• NeZero.charZero_one
• NeZero.mul
• NeZero.of_gt'
• NeZero.one
• NeZero.pnat
• NeZero.pow
• ZeroLEOneClass.neZero.four
• ZeroLEOneClass.neZero.three
• ZeroLEOneClass.neZero.two
• instNeZeroNatIte

theorem NeZero.ne {R : Type u_1} [Zero R] (n : R) [h : NeZero n] : n ≠ 0

theorem NeZero.ne' {R : Type u_1} [Zero R] (n : R) [h : NeZero n] : 0 ≠ n

theorem neZero_iff {R : Type u_1} [Zero R] {n : R} : NeZero n ↔ n ≠ 0

@[simp]

theorem neZero_zero_iff_false {α : Type u_1} [Zero α] : NeZero 0 ↔ False

instance instNeZeroNatIte {p : Prop} [Decidable p] {n m : Nat} [NeZero n] [NeZero m] : NeZero (if p then n else m)