two_ne_zero
theorem two_ne_zero : ∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 2] [inst_2 : NeZero 2], 2 ≠ 0
This theorem, named `two_ne_zero`, states that for any type `α` that has a zero element (`Zero α`), can interpret the natural number 2 (`OfNat α 2`), and 2 is not zero in that type (`NeZero 2`), two is not equal to zero (`2 ≠ 0`). In other words, it asserts that in any suitable mathematical structure, the number two cannot be the zero element.
More concisely: For any type with a zero element and where 2 is not zero, two is not equal to zero.
|
NeZero.ne
theorem NeZero.ne : ∀ {R : Type u_1} [inst : Zero R] (n : R) [h : NeZero n], n ≠ 0
This theorem, `NeZero.ne`, states that for any type `R` that has a zero element, any element `n` of `R` that is not zero, denoted by the property `NeZero n`, is not equal to zero. Here, `NeZero n` is a way of saying that `n` is non-zero, and `n ≠ 0` asserts that `n` is not equal to the zero element of `R`. In more traditional mathematical notation, this would read as "for all n in R, where R is any type with a zero, if n is not zero, then n is not equal to zero".
More concisely: For any type `R` with a zero element, every non-zero element `n` in `R` is distinct from the zero element.
|
zero_ne_one'
theorem zero_ne_one' : ∀ (α : Type u_2) [inst : Zero α] [inst_1 : One α] [inst_2 : NeZero 1], 0 ≠ 1
This theorem states that for any type `α` that has both zero and one elements and satisfies the property that one is not zero (signified by the `NeZero 1` instance), zero is not equal to one. This is generally applied to numeric types where the concepts of zero and one are well-defined, such as integers, real numbers, complex numbers, etc.
More concisely: For any type `α` with zero and one elements where one is not zero, zero is not equal to one. (In other words, `0 ≠ 1` for types `α` with `0` and `1` and `NeZero 1 α`.)
|
two_ne_zero'
theorem two_ne_zero' : ∀ (α : Type u_2) [inst : Zero α] [inst_1 : OfNat α 2] [inst_2 : NeZero 2], 2 ≠ 0
This theorem states that for any type `α` that has a zero element and can interpret the natural number 2, the number 2 is not equal to 0. The `NeZero 2` instance is a hypothesis that 2 is not zero in the type `α`. Basically, it asserts the non-equality between 2 and 0 in any such type. This theorem is a fundamental assumption in many areas of mathematics, particularly those involving arithmetic operations.
More concisely: If type `α` has a zero element and interprets the natural number 2, then 2 ≠ 0.
|
Mathlib.Algebra.NeZero._auxLemma.3
theorem Mathlib.Algebra.NeZero._auxLemma.3 :
∀ {α : Type u_2} [inst : Zero α] [inst_1 : One α] [inst_2 : NeZero 1], (0 = 1) = False
This theorem, referred to as `Mathlib.Algebra.NeZero._auxLemma.3`, states that for any type `α` (denoted as `u_2`) that has defined instances of zero (`inst`) and one (`inst_1`), and the number one is not equal to zero (`inst_2 : NeZero 1`), the proposition that zero equals one (`0 = 1`) is false. In other words, it ensures that, in the given algebraic context, zero and one are distinct entities.
More concisely: If `α` has defined instances of zero and one, and one is not equal to zero, then zero is not equal to one.
|
NeZero.of_pos
theorem NeZero.of_pos : ∀ {M : Type u_2} {x : M} [inst : Preorder M] [inst_1 : Zero M], 0 < x → NeZero x
This theorem, `NeZero.of_pos`, states that for any type `M` with a pre-order (`Preorder`) and a defined zero (`Zero`), if a value `x` of type `M` is greater than zero, then `x` is not equal to zero. In other words, any positive number in a preordered set with a defined zero is not equal to zero.
More concisely: If `x` is greater than zero in a preordered type `M` with defined zero, then `x ≠ 0`.
|
eq_zero_or_neZero
theorem eq_zero_or_neZero : ∀ {R : Type u_1} [inst : Zero R] (a : R), a = 0 ∨ NeZero a
This theorem, `eq_zero_or_neZero`, states that for any type `R` that has a `Zero` instance (essentially, a type that has a concept of "zero"), any element `a` of type `R` either equals zero (`a = 0`) or it does not equal zero (`NeZero a`), where `NeZero a` is a predicate that is true when `a` is not equal to zero. This is a basic law of logic and arithmetic, asserting the dichotomy that any number is either zero or not zero.
More concisely: For any type `R` with a `Zero` instance, every `a` in `R` is either equal to zero or not equal to zero.
|
zero_ne_one
theorem zero_ne_one : ∀ {α : Type u_2} [inst : Zero α] [inst_1 : One α] [inst_2 : NeZero 1], 0 ≠ 1
This theorem, named `zero_ne_one`, is a statement about any type `α` that has a zero (`Zero α`), a one (`One α`), and the property that one is not zero (`NeZero 1`). It asserts that zero is not equal to one in the given type. This is a fundamental property in mathematics and is usually employed in fields where the concept of zero and one are defined such as in the case of numbers.
More concisely: For any type `α` with `Zero α`, `One α`, and `NeZero 1`, `Zero α` is not equal to `One α`.
|
neZero_iff
theorem neZero_iff : ∀ {R : Type u_1} [inst : Zero R] {n : R}, NeZero n ↔ n ≠ 0
The theorem `neZero_iff` states that for any type `R` with a zero element, an element `n` of type `R` is non-zero (as defined by the predicate `NeZero`) if and only if `n` is not equal to `0`. This is a universal statement applicable to any type `R` which has a defined zero element.
More concisely: For any type `R` with a zero element, an element `n` of type `R` is non-zero (as defined in Lean) if and only if `n` is distinct from the zero element of `R`.
|
ne_zero_of_eq_one
theorem ne_zero_of_eq_one :
∀ {α : Type u_2} [inst : Zero α] [inst_1 : One α] [inst_2 : NeZero 1] {a : α}, a = 1 → a ≠ 0
This theorem states that for any type `α` that has both zero and one elements (denoted by `0` and `1` respectively), if an element `a` of this type equals `1`, then it cannot equal `0`. In mathematical terms, for any element `a` in a set where `0` and `1` are defined and distinct, if `a = 1` then `a ≠ 0`.
More concisely: For any type with defined and distinct zero and one elements, an element equal to one is not equal to zero.
|
Mathlib.Algebra.NeZero._auxLemma.4
theorem Mathlib.Algebra.NeZero._auxLemma.4 :
∀ {α : Type u_2} [inst : Zero α] [inst_1 : One α] [inst_2 : NeZero 1], (1 = 0) = False
This theorem, named `_auxLemma.4` in the `Mathlib.Algebra.NeZero` module, states that for any type `α` where `α` has the properties of zero and one and `1` is not equal to `0`, it is always false that `1` equals `0`. In other words, in any algebraic system where `1` and `0` are distinct, `1` cannot be equal to `0`.
More concisely: In any algebraic system where `1` and `0` are distinct objects, `1` is not equal to `0`.
|
one_ne_zero
theorem one_ne_zero : ∀ {α : Type u_2} [inst : Zero α] [inst_1 : One α] [inst_2 : NeZero 1], 1 ≠ 0
This theorem simply states that one is not equal to zero. It is generalized to any type `α` that has defined zero and one values, under the condition that `α` also has the property `NeZero 1`, meaning that one as defined in `α` is not zero. In mathematical terms, this can be expressed as ∀α. 1_α ≠ 0_α.
More concisely: For all types `α` with defined zero and one values, and where `α` has the property `NeZero 1`, one (1\_α) is not equal to zero (0\_α).
|
one_ne_zero'
theorem one_ne_zero' : ∀ (α : Type u_2) [inst : Zero α] [inst_1 : One α] [inst_2 : NeZero 1], 1 ≠ 0
This theorem states that for every data type `α`, given that this type has a zero element (as provided by the `Zero α` instance), a one element (given by `One α` instance), and that it's not possible for one to be equal to zero in type `α` (given by the `NeZero 1` instance), then one is not equal to zero in this type. In mathematical terms, this theorem asserts that ∀α, 1 ≠ 0 in the context where α has a zero, a one, and one is not equal to zero.
More concisely: If type `α` has a zero element, a one element, and one is not equal to zero, then one is not equal to zero in `α`. In symbols, `∀α (Zero α : α) (One α : α) (NeZero 1 α : One α ≠ Zero α) : One α ≠ Zero α`.
|
NeZero.out
theorem NeZero.out : ∀ {R : Type u_1} [inst : Zero R] {n : R} [self : NeZero n], n ≠ 0
This theorem is a statement about a non-zero element `n` in a type `R` that has a `Zero` instance. Specifically, it asserts that `n` is not equal to zero. Essentially, for any type `R` that has an instance of the `Zero` class (meaning it has a defined `0` element), and any element `n` of that type which is not zero, this theorem verifies that `n` is indeed not equal to zero.
More concisely: For any type `R` with a `Zero` instance and non-zero element `n`, `n ≠ 0`.
|