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

• Nat.instNeZeroHPow
• Nat.instNeZeroSucc

theorem NeZero.out {R : Type u_1} : ∀ {inst : Zero R} {n : R} [self : NeZero n], n ≠ 0

The proposition that n is not zero.

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