Mathlib.Algebra.NeZero

not_neZero theorem

{n : R} : ¬NeZero n ↔ n = 0

Full source

theorem not_neZero {n : R} : ¬NeZero n¬NeZero n ↔ n = 0 := by simp [neZero_iff]

Characterization of Non-Zero Elements: $\neg \text{NeZero}\, n \leftrightarrow n = 0$

Informal description

For an element $n$ of a type $R$, the predicate $\text{NeZero}\, n$ does not hold if and only if $n = 0$.

zero_ne_one theorem

[One α] [NeZero (1 : α)] : (0 : α) ≠ 1

Full source

@[simp] lemma zero_ne_one [One α] [NeZero (1 : α)] : (0 : α) ≠ 1 := NeZero.ne' (1 : α)

Nonzero Identity: $0 \neq 1$ in a `NeZero` context

Informal description

For any type $\alpha$ with a multiplicative identity $1$ and a `NeZero` instance for $1$, it holds that $0 \neq 1$.

one_ne_zero theorem

[One α] [NeZero (1 : α)] : (1 : α) ≠ 0

Full source

@[simp] lemma one_ne_zero [One α] [NeZero (1 : α)] : (1 : α) ≠ 0 := NeZero.ne (1 : α)

Nonzero Identity: $1 \neq 0$ under `NeZero` condition

Informal description

For any type $\alpha$ with a multiplicative identity element $1$ and a `NeZero` instance ensuring that $1$ is not zero, we have $1 \neq 0$.

ne_zero_of_eq_one theorem

[One α] [NeZero (1 : α)] {a : α} (h : a = 1) : a ≠ 0

Full source

lemma ne_zero_of_eq_one [One α] [NeZero (1 : α)] {a : α} (h : a = 1) : a ≠ 0 := h ▸ one_ne_zero

Nonzero Property via Identity: $a = 1 \implies a \neq 0$ under `NeZero` condition

Informal description

For any type $\alpha$ with a multiplicative identity $1$ and a `NeZero` instance ensuring that $1$ is not zero, if an element $a$ of $\alpha$ satisfies $a = 1$, then $a \neq 0$.

two_ne_zero theorem

[OfNat α 2] [NeZero (2 : α)] : (2 : α) ≠ 0

Full source

@[field_simps]
lemma two_ne_zero [OfNat α 2] [NeZero (2 : α)] : (2 : α) ≠ 0 := NeZero.ne (2 : α)

Nonzero Property of Two: $2 \neq 0$

Informal description

For any type $\alpha$ with a distinguished element $2$ (via `OfNat`) and satisfying `NeZero (2 : α)`, the element $2$ is not equal to $0$.

three_ne_zero theorem

[OfNat α 3] [NeZero (3 : α)] : (3 : α) ≠ 0

Full source

@[field_simps]
lemma three_ne_zero [OfNat α 3] [NeZero (3 : α)] : (3 : α) ≠ 0 := NeZero.ne (3 : α)

Nonzero Property of Three: $3 \neq 0$

Informal description

For any type $\alpha$ with a canonical element `3` (via `OfNat`) and a proof that `3` is not zero (`NeZero (3 : α)`), we have that `3 ≠ 0` in $\alpha$.

four_ne_zero theorem

[OfNat α 4] [NeZero (4 : α)] : (4 : α) ≠ 0

Full source

@[field_simps]
lemma four_ne_zero [OfNat α 4] [NeZero (4 : α)] : (4 : α) ≠ 0 := NeZero.ne (4 : α)

Nonzero Property of Four: $4 \neq 0$

Informal description

For any type $\alpha$ with a `OfNat` instance for the natural number 4 and a `NeZero` instance ensuring that 4 is not zero, the element $4 : \alpha$ is not equal to zero, i.e., $4 \neq 0$.

zero_ne_one' theorem

[One α] [NeZero (1 : α)] : (0 : α) ≠ 1

Full source

lemma zero_ne_one' [One α] [NeZero (1 : α)] : (0 : α) ≠ 1 := zero_ne_one

Nonzero Identity: $0 \neq 1$ in a `NeZero` context

Informal description

For any type $\alpha$ with a multiplicative identity $1$ and a `NeZero` instance for $1$, it holds that $0 \neq 1$.

one_ne_zero' theorem

[One α] [NeZero (1 : α)] : (1 : α) ≠ 0

Full source

lemma one_ne_zero' [One α] [NeZero (1 : α)] : (1 : α) ≠ 0 := one_ne_zero

Nonzero Identity: $1 \neq 0$ under `NeZero` condition

Informal description

For any type $\alpha$ with a multiplicative identity element $1$ and a `NeZero` instance ensuring that $1$ is not zero, we have $1 \neq 0$.

two_ne_zero' theorem

[OfNat α 2] [NeZero (2 : α)] : (2 : α) ≠ 0

Full source

lemma two_ne_zero' [OfNat α 2] [NeZero (2 : α)] : (2 : α) ≠ 0 := two_ne_zero

Nonzero Property of Two: $2 \neq 0$

Informal description

For any type $\alpha$ with a distinguished element $2$ (via `OfNat`) and satisfying `NeZero (2 : α)`, the element $2$ is not equal to $0$, i.e., $2 \neq 0$.

three_ne_zero' theorem

[OfNat α 3] [NeZero (3 : α)] : (3 : α) ≠ 0

Full source

lemma three_ne_zero' [OfNat α 3] [NeZero (3 : α)] : (3 : α) ≠ 0 := three_ne_zero

Nonzero Property of Three: $3 \neq 0$

Informal description

For any type $\alpha$ with a canonical element $3$ (via `OfNat`) and a proof that $3$ is not zero (`NeZero (3 : \alpha)`), we have that $3 \neq 0$ in $\alpha$.

four_ne_zero' theorem

[OfNat α 4] [NeZero (4 : α)] : (4 : α) ≠ 0

Full source

lemma four_ne_zero' [OfNat α 4] [NeZero (4 : α)] : (4 : α) ≠ 0 := four_ne_zero

Nonzero Property of Four: $4 \neq 0$

Informal description

For any type $\alpha$ with a `OfNat` instance for the natural number 4 and a `NeZero` instance ensuring that 4 is not zero, the element $4 : \alpha$ is not equal to zero, i.e., $4 \neq 0$.

NeZero.of_pos theorem

[Preorder M] [Zero M] (h : 0 < x) : NeZero x

Full source

theorem of_pos [Preorder M] [Zero M] (h : 0 < x) : NeZero x := ⟨ne_of_gt h⟩

Positivity Implies Nonzero in Ordered Structures

Informal description

For any type $M$ with a preorder and a zero element, if $0 < x$ for some $x : M$, then $x$ is nonzero (i.e., $x \neq 0$).