Init.Data.NeZero

NeZero structure

(n : R)

Full source

/-- A type-class version of `n ≠ 0`.  -/
class NeZero (n : R) : Prop where
  /-- The proposition that `n` is not zero. -/
  out : n ≠ 0

Non-zero element typeclass

Informal description

A typeclass that asserts a given element `n` of type `R` is not equal to zero. This is used to conveniently carry around the fact that `n ≠ 0` in a typeclass instance.

NeZero.ne theorem

(n : R) [h : NeZero n] : n ≠ 0

Full source

theorem NeZero.ne (n : R) [h : NeZero n] : n ≠ 0 :=
  h.out

Non-zero element is non-zero

Informal description

For any element $n$ of type $R$ with a `NeZero` instance, we have $n \neq 0$.

NeZero.ne' theorem

(n : R) [h : NeZero n] : 0 ≠ n

Full source

theorem NeZero.ne' (n : R) [h : NeZero n] : 0 ≠ n :=
  h.out.symm

Non-zero element is non-zero (symmetric form)

Informal description

For any element $n$ of type $R$ with a `NeZero` instance, we have $0 \neq n$.

neZero_iff theorem

{n : R} : NeZero n ↔ n ≠ 0

Full source

theorem neZero_iff {n : R} : NeZeroNeZero n ↔ n ≠ 0 :=
  ⟨fun h ↦ h.out, NeZero.mk⟩

Equivalence of `NeZero` and Non-Zero Condition

Informal description

For any element $n$ of type $R$, the typeclass `NeZero n` holds if and only if $n \neq 0$.

neZero_zero_iff_false theorem

{α : Type _} [Zero α] : NeZero (0 : α) ↔ False

Full source

@[simp] theorem neZero_zero_iff_false {α : Type _} [Zero α] : NeZeroNeZero (0 : α) ↔ False :=
  ⟨fun _ ↦ NeZero.ne (0 : α) rfl, fun h ↦ h.elim⟩

`NeZero` of Zero is Equivalent to False

Informal description

For any type $\alpha$ with a zero element, the typeclass `NeZero (0 : α)` holds if and only if `False`.

instNeZeroNatIte instance

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

Full source

instance {p : Prop} [Decidable p] {n m : Nat} [NeZero n] [NeZero m] :
    NeZero (if p then n else m) := by
  split <;> infer_instance

Non-Zero Property Preserved by Conditional on Natural Numbers

Informal description

For any proposition $p$ with a decidable instance, and natural numbers $n$ and $m$ that are both non-zero, the conditional expression `if p then n else m` is also non-zero.

instNeZeroNatHAdd instance

{n m : Nat} [h : NeZero n] : NeZero (n + m)

Full source

instance {n m : Nat} [h : NeZero n] : NeZero (n + m) where
  out :=
    match n, h, m with
    | _ + 1, _, 0
    | _ + 1, _, _ + 1 => fun h => nomatch h

Nonzero Natural Numbers Remain Nonzero Under Addition

Informal description

For any natural numbers $n$ and $m$, if $n$ is nonzero, then $n + m$ is also nonzero.

instNeZeroNatHAdd_1 instance

{n m : Nat} [h : NeZero m] : NeZero (n + m)

Full source

instance {n m : Nat} [h : NeZero m] : NeZero (n + m) where
  out :=
    match m, h, n with
    | _ + 1, _, 0 => fun h => nomatch h
    | _ + 1, _, _ + 1 => fun h => nomatch h

Nonzero Sum of Natural Numbers (Right Term Nonzero)

Informal description

For any natural numbers $n$ and $m$, if $m$ is nonzero, then $n + m$ is also nonzero.

instNeZeroNatHMul instance

{n m : Nat} [hn : NeZero n] [hm : NeZero m] : NeZero (n * m)

Full source

instance {n m : Nat} [hn : NeZero n] [hm : NeZero m] : NeZero (n * m) where
  out :=
    match n, hn, m, hm with
    | _ + 1, _, _ + 1, _ => fun h => nomatch h

Nonzero Product of Natural Numbers

Informal description

For any natural numbers $n$ and $m$, if both $n$ and $m$ are nonzero, then their product $n * m$ is also nonzero.

Main declarations