subsingleton_iff_zero_eq_one
theorem subsingleton_iff_zero_eq_one : ∀ {M₀ : Type u_2} [inst : MulZeroOneClass M₀], 0 = 1 ↔ Subsingleton M₀ := by
sorry
This theorem states that in a monoid with zero (a mathematical structure where multiplication, zero, and one are defined), zero is equal to one if and only if all elements in the semiring (a generalization of rings in algebra) are the same. In other words, in such a monoid, if zero and one are indistinguishable, then every other element in that semiring is also indistinguishable.
More concisely: In a monoid with zero, zero is equal to one if and only if all elements are equal.
|
mul_inv_mul_self
theorem mul_inv_mul_self : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] (a : G₀), a * a⁻¹ * a = a
This theorem states that for any type `G₀` that has the structure of a group with zero, multiplying any element `a` from this group by its inverse and then by `a` again, results in `a`. This holds true regardless of whether `a` is zero or not. In mathematical terms, for any `a` in `G₀`, we have `a * a⁻¹ * a = a`.
More concisely: For any group `G₀` with zero and any element `a` in `G₀`, `a * a⁻¹ * a = a`.
|
Mathlib.Algebra.GroupWithZero.Basic._auxLemma.1
theorem Mathlib.Algebra.GroupWithZero.Basic._auxLemma.1 :
∀ {M₀ : Type u_2} [inst : Mul M₀] [inst_1 : Zero M₀] [inst_2 : NoZeroDivisors M₀] {a b : M₀},
a ≠ 0 → b ≠ 0 → (a * b = 0) = False
The theorem `Mathlib.Algebra.GroupWithZero.Basic._auxLemma.1` states that, for any type `M₀`, given a multiplication operation, a zero element, and the condition that there are no zero divisors, if `a` and `b` are elements of `M₀` and neither `a` nor `b` is equal to zero, then the statement that the product of `a` and `b` equals zero is always false. In other words, in a type with multiplication, zero, and no zero divisors, the product of any two non-zero elements cannot be zero.
More concisely: In a group with multiplication and a zero element, without zero divisors, the product of any two non-zero elements is never zero.
|
zero_ne_one_or_forall_eq_0
theorem zero_ne_one_or_forall_eq_0 : ∀ {M₀ : Type u_2} [inst : MulZeroOneClass M₀], 0 ≠ 1 ∨ ∀ (a : M₀), a = 0 := by
sorry
This theorem states that in any monoid with zero (a set in which multiplication and an identity element are defined and an element representing zero exists), either the identity element (one) and zero are different, or every element in the monoid is equal to zero.
More concisely: In any monoid with an identity and zero, if the identity is not equal to zero, then every element is distinct from zero; otherwise, every element is equal to zero.
|
left_ne_zero_of_mul_eq_one
theorem left_ne_zero_of_mul_eq_one :
∀ {M₀ : Type u_2} [inst : MulZeroOneClass M₀] [inst_1 : Nontrivial M₀] {a b : M₀}, a * b = 1 → a ≠ 0
This theorem states that for any type `M₀` that has a multiplication operation, a zero element, and a one element (i.e., belongs to the `MulZeroOneClass`), and is nontrivial (i.e., not every element is equal to every other), if the product of two elements `a` and `b` equals one, then `a` cannot be zero.
More concisely: If `M₀` is a nontrivial type with multiplication, zero, and one, then `a * b = 1` implies `a ≠ 0`.
|
mul_eq_mul_left_iff
theorem mul_eq_mul_left_iff :
∀ {M₀ : Type u_2} [inst : CancelMonoidWithZero M₀] {a b c : M₀}, a * b = a * c ↔ b = c ∨ a = 0
This theorem states that for any type `M₀` that forms a `CancelMonoidWithZero` (a mathematical structure with a multiplication operation and an element '0' such that multiplication by '0' yields '0'), and for any elements `a`, `b`, `c` of this type, the equality `a * b = a * c` is equivalent to the condition that `b` equals `c` or `a` equals '0'. In other words, if `a` is not '0', `a * b = a * c` implies `b = c`; but if `a` is '0', `a * b = a * c` holds true for any `b` and `c`.
More concisely: For any `CancelMonoidWithZero` type `M₀` and elements `a` and `b` of `M₀`, if `a ≠ 0`, then `a * b = a * c` implies `b = c`. If `a = 0`, then `a * b = a * c` holds for all `b` and `c`.
|
zero_div
theorem zero_div : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] (a : G₀), 0 / a = 0
This theorem states that for any type `G₀` that has the structure of a group with zero (i.e., it is equipped with an operation and a zero element such that it behaves like a mathematical group with an additional zero element), the division of zero by any element `a` of `G₀` is zero. In mathematical terms, this theorem simply states the universal property that zero divided by anything equals zero in a group with zero.
More concisely: In a group with zero, the product of any element with zero is zero.
|
pow_eq_zero
theorem pow_eq_zero :
∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {a : M₀} [inst_1 : NoZeroDivisors M₀] {n : ℕ}, a ^ n = 0 → a = 0 := by
sorry
The theorem `pow_eq_zero` states that for any type `M₀` that has a structure of a monoid with zero and no zero divisors, if a number `a` of type `M₀` raised to the power `n` (where `n` is a natural number) is equal to zero, then `a` must be zero. This theorem essentially formalizes the intuitive mathematical concept that only zero, when raised to a positive power, can result in zero.
More concisely: If `a` is an element of a monoid with zero and no zero divisors such that `a^n = 0` for some natural number `n`, then `a = 0`.
|
zero_mul_eq_const
theorem zero_mul_eq_const : ∀ {M₀ : Type u_2} [inst : MulZeroClass M₀], (fun x => 0 * x) = Function.const M₀ 0 := by
sorry
This theorem states that for any type `M₀` that is a multiplicative group with zero (i.e., it supports multiplication and has a zero element such that any element times zero yields zero), the function that multiplies each element of `M₀` by zero is the same as the constant function that always returns zero. In mathematical terms, for all `x` in `M₀`, `0 * x` is always `0`, which is the same result as the constant function with value `0`.
More concisely: For any multiplicative group with zero `M₀`, the multiplication-by-zero function equals the constant function with value `0`. In other words, for all `x` in `M₀`, `0 * x = 0`.
|
inv_mul_cancel_right₀
theorem inv_mul_cancel_right₀ :
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {b : G₀}, b ≠ 0 → ∀ (a : G₀), a * b⁻¹ * b = a
This theorem states that for any non-zero element `b` of a group with zero `G₀`, and for any element `a` of the same group, the product of `a`, the inverse of `b` and `b` is equal to `a`. This essentially captures the property that multiplying by an element and its inverse (in the given order) in a group with zero acts as an identity operation.
More concisely: For any group with zero `G₀` and any `a, b` in `G₀^*, a * b^(-1) * b = a`, where `*` denotes group multiplication and `^(-1)` denotes group inversion.
|
Mathlib.Algebra.GroupWithZero.Basic._auxLemma.15
theorem Mathlib.Algebra.GroupWithZero.Basic._auxLemma.15 :
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, (a⁻¹ = 0) = (a = 0)
This theorem, named `Mathlib.Algebra.GroupWithZero.Basic._auxLemma.15`, states that for any type `G₀` that has a GroupWithZero structure, the inverse `a⁻¹` of any element `a` of `G₀` is zero if and only if `a` itself is zero. In the context of algebra, a GroupWithZero is a group with an additional zero element that is distinct from the identity and annihilates the group under multiplication.
More concisely: For any GroupWithZero type `G₀`, the inverse of an element `a` is zero if and only if `a` itself is the zero element.
|
inv_mul_cancel_left₀
theorem inv_mul_cancel_left₀ :
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → ∀ (b : G₀), a⁻¹ * (a * b) = b
This theorem states that for any type `G₀` that has a structure of a group with zero, for any non-zero element `a` of type `G₀` and any `b` of type `G₀`, the inverse of `a` multiplied by the product of `a` and `b` equals `b`. In mathematical terms, it states that if $a$ is not zero, then $a^{-1}(ab) = b$. This is a fundamental property of groups where the multiplication of an element by its inverse results in the identity, in this case the identity being such that multiplying any element by it leaves the element unchanged.
More concisely: For any group with zero `G₀` and non-zero element `a` in `G₀`, `a`'s inverse multiplied by the product of `a` and any element `b` in `G₀` equals `b`. In mathematical notation, $a^{-1}(ab) = b$.
|
div_self_mul_self'
theorem div_self_mul_self' : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] (a : G₀), a / (a * a) = a⁻¹
This theorem asserts that for every element `a` in a group with zero `G₀`, the result of dividing `a` by the product of `a` with itself (`a * a`) is equal to the inverse of `a`. In mathematical notation, this theorem is saying that for any `a` in the group with zero `G₀`, it follows that `a / (a * a) = a⁻¹`. It's important to note that this theorem is only valid in the context of a group with zero, which is a mathematical structure that extends the concept of a group by including a zero element.
More concisely: In a group with zero, for all `a` in the group, `a / (a * a) = a⁻¹`.
|
pow_eq_zero_iff
theorem pow_eq_zero_iff :
∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {a : M₀} {n : ℕ} [inst_1 : NoZeroDivisors M₀],
n ≠ 0 → (a ^ n = 0 ↔ a = 0)
This theorem, `pow_eq_zero_iff`, states that for any non-zero natural number `n` and any element `a` from a monoid with zero and no zero divisors (a mathematical structure like integers, real numbers, etc.), `a` raised to the power `n` is zero if and only if `a` itself is zero. In other words, in such a structure, a non-zero power of a value can only be zero if the value itself is zero.
More concisely: For any non-zero natural number `n` and any element `a` in a monoid with zero and no zero divisors, `a^n = 0` if and only if `a = 0`.
|
mul_ne_zero
theorem mul_ne_zero :
∀ {M₀ : Type u_2} [inst : Mul M₀] [inst_1 : Zero M₀] [inst_2 : NoZeroDivisors M₀] {a b : M₀},
a ≠ 0 → b ≠ 0 → a * b ≠ 0
This theorem states that for any type `M₀` which has a multiplication operation, a zero element, and has no zero divisors, if `a` and `b` are elements of `M₀` such that neither `a` nor `b` is zero, then the product of `a` and `b` is also not zero. This is a generalization of a well-known property from number theory: the product of two non-zero numbers is always non-zero.
More concisely: In a type with multiplication, zero element, and no zero divisors, the product of two non-zero elements is non-zero.
|
Mathlib.Algebra.GroupWithZero.Basic._auxLemma.3
theorem Mathlib.Algebra.GroupWithZero.Basic._auxLemma.3 :
∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {a : M₀} {n : ℕ} [inst_1 : NoZeroDivisors M₀],
n ≠ 0 → (a ^ n = 0) = (a = 0)
This theorem, `Mathlib.Algebra.GroupWithZero.Basic._auxLemma.3`, states that for any `MonoidWithZero` (a mathematical structure that is a monoid, meaning it has an associative binary operation and an identity element, and also has a zero element distinct from the identity), in which there are no zero divisors (pairs of nonzero elements that multiply to zero), if we have a nonzero natural number `n` and an element `a` of this structure, then `a` raised to the power of `n` equals zero if and only if `a` equals zero.
More concisely: For any MonoidWithZero without zero divisors, if a nonzero element a raised to the power of a natural number n equals zero, then a equals zero.
|
div_zero
theorem div_zero : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] (a : G₀), a / 0 = 0
This theorem states that for any type `G₀`, which has an instance of the `GroupWithZero` structure, the result of dividing any element `a` of this type by zero is zero. In mathematical terms, for any group with zero (a mathematical structure that is a group, but also has a zero element and satisfies certain properties), the division of any element of the group by zero yields zero.
More concisely: For any group with zero `G₀`, `0 * x = x * 0 => x = 0` for all `x` in `G₀`. (In other words, dividing any element of `G₀` by zero results in zero.)
|
eq_zero_of_mul_self_eq_zero
theorem eq_zero_of_mul_self_eq_zero :
∀ {M₀ : Type u_2} [inst : Mul M₀] [inst_1 : Zero M₀] [inst_2 : NoZeroDivisors M₀] {a : M₀}, a * a = 0 → a = 0 := by
sorry
This theorem states that for any type `M₀` which has a multiplication operation, a zero element, and no zero divisors, if a member `a` of `M₀` satisfies the property that the multiplication of `a` with itself equals zero, then `a` itself must be zero. Essentially, this is a formalization of the mathematical principle that the square of a non-zero number is never zero.
More concisely: If `M₀` is a type with multiplication, zero, and no zero divisors, then for all `a` in `M₀`, `a * a = 0` implies `a = 0`.
|
mul_zero_eq_const
theorem mul_zero_eq_const : ∀ {M₀ : Type u_2} [inst : MulZeroClass M₀], (fun x => x * 0) = Function.const M₀ 0 := by
sorry
The theorem `mul_zero_eq_const` is a statement about a specific property of multiplication in a mathematical structure, specifically a structure (type `M₀`) that is a member of the `MulZeroClass`. The `MulZeroClass` means that the structure `M₀` has a multiplication operation and a zero element, and the multiplication operation obeys the property that anything multiplied by zero equals zero. This theorem states that for all elements 'x' of the type `M₀`, the function which multiplies 'x' by zero is equal to the constant function that always returns zero. In simpler terms, this theorem formalizes the familiar arithmetic fact that anything multiplied by zero is zero.
More concisely: For all elements x in a MulZeroClass algebra, x * 0 = 0.
|
sq_eq_zero_iff
theorem sq_eq_zero_iff :
∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {a : M₀} [inst_1 : NoZeroDivisors M₀], a ^ 2 = 0 ↔ a = 0
This theorem states that for any type `M₀` that is a Monoid with zero and has no zero divisors, the square of an element `a` from `M₀` equals to zero if and only if `a` equals to zero. In other words, in a given Monoid with zero and no zero divisors, the only square that is zero is the zero itself.
More concisely: In a Monoid with zero and no zero divisors, the square of any element equals zero if and only if the element is the zero.
|
eq_zero_of_mul_eq_self_left
theorem eq_zero_of_mul_eq_self_left :
∀ {M₀ : Type u_2} [inst : CancelMonoidWithZero M₀] {a b : M₀}, b ≠ 1 → b * a = a → a = 0
This theorem states that for any type `M₀` that is a `CancelMonoidWithZero`, if we have two elements `a` and `b` of `M₀` such that `b` is not equal to 1, and the result of multiplying `b` and `a` equals `a`, then `a` must be equal to 0. In mathematical terms, within a cancel monoid with zero, if we have $b \neq 1$ and $b*a = a$, then it must be the case that $a = 0$.
More concisely: In a cancel monoid with zero, if $b \neq 1$ and $b \cdot a = a$, then $a = 0$.
|
subsingleton_of_zero_eq_one
theorem subsingleton_of_zero_eq_one : ∀ {M₀ : Type u_2} [inst : MulZeroOneClass M₀], 0 = 1 → Subsingleton M₀
This theorem, `subsingleton_of_zero_eq_one`, states that in a monoid with zero (a mathematical structure, denoted by `M₀`, with a multiplication operation, a zero, and a one), if zero equals one, then all elements of this monoid are the same (i.e., it's a subsingleton). A monoid with zero is a particular type of mathematical structure that includes both multiplication operation and a zero element. This theorem represents one direction of a logical equivalence, namely that if zero equals one in such a structure, then every element in the structure is equal to every other.
More concisely: In a monoid with zero, if zero equals one, then all elements are equal.
|
right_ne_zero_of_mul
theorem right_ne_zero_of_mul : ∀ {M₀ : Type u_2} [inst : MulZeroClass M₀] {a b : M₀}, a * b ≠ 0 → b ≠ 0
This theorem states that for any type `M₀` equipped with a multiplication operation and a zero element (i.e., a `MulZeroClass`), if the product of two elements `a` and `b` is not zero, then `b` cannot be zero. In mathematical terms, for all `a` and `b` in `M₀`, if `a * b ≠ 0`, then it must be the case that `b ≠ 0`. This statement implicitly relies on the property of zero in a `MulZeroClass` that anything multiplied by zero equals zero.
More concisely: If `M₀` is a type with a multiplication operation and a zero element, and `a * b ≠ 0`, then `b ≠ 0` in `M₀`.
|
eq_zero_of_mul_eq_self_right
theorem eq_zero_of_mul_eq_self_right :
∀ {M₀ : Type u_2} [inst : CancelMonoidWithZero M₀] {a b : M₀}, b ≠ 1 → a * b = a → a = 0
This theorem states that for any type `M₀` that is a `CancelMonoidWithZero`, given two elements `a` and `b` of `M₀`, if `b` is not equal to 1 and the multiplication of `a` with `b` equals `a`, then `a` must be zero. In other words, if multiplying `a` with an element other than 1 doesn't change `a`, then `a` must be the zero element of the `CancelMonoidWithZero`.
More concisely: If `a` is an element of a `CancelMonoidWithZero` `M₀` such that `b ≠ 1` and `a * b = a`, then `a` is the zero element of `M₀`.
|
inv_eq_zero
theorem inv_eq_zero : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, a⁻¹ = 0 ↔ a = 0
This theorem states that for any given type `G₀` that has a structure of a group with zero (i.e., a group that includes a zero element), an element `a` of `G₀` has its inverse equal to zero if and only if `a` itself is zero. In other words, for such types, an element is zero if its inverse is zero, and vice versa. This theorem is a fundamental property in the theory of groups with zero.
More concisely: In a group with zero, an element is zero if and only if its inverse is zero.
|
pow_ne_zero
theorem pow_ne_zero :
∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {a : M₀} [inst_1 : NoZeroDivisors M₀] (n : ℕ), a ≠ 0 → a ^ n ≠ 0 := by
sorry
This theorem states that for any non-zero element `a` of a given type `M₀` (which forms a Monoid with zero and has no zero divisors), the power of `a` raised to any natural number `n` is not equal to zero. This means, in such a structure, a non-zero element raised to any power never results in zero.
More concisely: For any non-zero element `a` in a Monoid `M₀` without zero divisors, `a^n ≠ 0` for all natural numbers `n`.
|
Mathlib.Algebra.GroupWithZero.Basic._auxLemma.7
theorem Mathlib.Algebra.GroupWithZero.Basic._auxLemma.7 :
∀ {M₀ : Type u_2} [inst : CancelMonoidWithZero M₀] {a b c : M₀}, (a * c = b * c) = (a = b ∨ c = 0)
This theorem states that for any type `M₀`, provided it is a cancellation monoid with zero, and for any elements `a`, `b`, and `c` of this type, the equality `a * c = b * c` is equivalent to the statement `a = b` or `c = 0`. In other words, if multiplication of `a` and `c` equals multiplication of `b` and `c`, then either `a` and `b` are equal or `c` is zero.
More concisely: For any cancellation monoid with zero `M₀`, the equality `a * c = b * c` implies `a = b` or `c = 0`.
|
left_ne_zero_of_mul
theorem left_ne_zero_of_mul : ∀ {M₀ : Type u_2} [inst : MulZeroClass M₀] {a b : M₀}, a * b ≠ 0 → a ≠ 0
This theorem states that for any type `M₀` that has a multiplication and zero structure (i.e., a `MulZeroClass`), if the product of two elements `a` and `b` is not zero, then `a` cannot be zero. In other words, in any multiplication operation, if the product is non-zero, then none of the multiplicands can be zero.
More concisely: If `M₀` is a type with a multiplication and zero structure, then for all `a` and `b` in `M₀`, `a ≠ 0` implies `a * b ≠ 0`.
|
div_div_self
theorem div_div_self : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] (a : G₀), a / (a / a) = a
This theorem states that for any type `G₀` that forms a group with zero, for any element `a` of that type, dividing `a` by the result of dividing `a` by itself gives `a` back. This holds true even if `a` is zero. In mathematical terms, for any `a` in `G₀`, `(a / (a / a))` equals `a`.
More concisely: For any group `G₀` with identity `0`, and for any `a` in `G₀`, `(a / (a % a)) = a`. (Here, `%` denotes division in Lean, and `a % a` is the multiplicative inverse of `a` when it exists, and `0` otherwise.)
|
inv_mul_mul_self
theorem inv_mul_mul_self : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] (a : G₀), a⁻¹ * a * a = a
This theorem states that for any type `G₀` that is a group with a zero element, the result of multiplying the multiplicative inverse of an element `a` by `a` twice is equal to `a`, regardless of whether `a` is zero or not. In mathematical terms, for any `a` in `G₀`, we have `(a⁻¹ * a) * a = a`.
More concisely: For any group `G₀` with identity element and for all `a` in `G₀`, `(a^(-1) * a) * a = a`.
|
mul_self_mul_inv
theorem mul_self_mul_inv : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] (a : G₀), a * a * a⁻¹ = a
This theorem states that for any element `a` of a group with zero, multiplying `a` by itself and then by its inverse will yield `a` as the result. This rule applies regardless of whether `a` is zero or not. In mathematical notation, this can be expressed as: for all `a` in the GroupWithZero `G₀`, `a * a * a⁻¹ = a`.
More concisely: For all elements `a` in a group with zero, `a * a * a⁻¹ = a`. (Alternatively, for all `a` in a group with identity `e`, `a * a * a⁻¹ = a * e * a = a`)
|
zero_pow_eq
theorem zero_pow_eq : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] (n : ℕ), 0 ^ n = if n = 0 then 1 else 0
This theorem states that for any natural number `n` and a type `M₀` that is a monoid with zero, the power of 0 raised to `n` (`0 ^ n`) equates to 1 if `n` equals zero (`n = 0`), else it equates to zero. Essentially, it's defining the outcome of zero raised to any natural number, following the mathematical convention that zero to the power of zero is defined as one, and zero to the power of any other natural number is zero.
More concisely: For any monoid with zero `M₀` and natural number `n`, `0 ^ n = 1` if `n = 0`, otherwise `0 ^ n = 0`.
|
right_ne_zero_of_mul_eq_one
theorem right_ne_zero_of_mul_eq_one :
∀ {M₀ : Type u_2} [inst : MulZeroOneClass M₀] [inst_1 : Nontrivial M₀] {a b : M₀}, a * b = 1 → b ≠ 0
This theorem states that, for any instance of a `MulZeroOneClass` type `M₀` where `M₀` is nontrivial (i.e., it has at least two distinct elements), if the product of two elements `a` and `b` equals one, then `b` cannot be zero. In other words, in such a system, any element that when multiplied by another element yields one, must itself be nonzero.
More concisely: If `MulZeroOneClass` `M₀` has at least two distinct elements, then for all `a` and `b` in `M₀`, `a * b = 1` implies `b ≠ 0`.
|
div_self_mul_self
theorem div_self_mul_self : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] (a : G₀), a / a * a = a
This theorem states that for any element `a` in a group with zero `G₀`, the operation of dividing `a` by itself and then multiplying by itself will result in `a`. This is true regardless of whether `a` is zero or not. In mathematical terms, it expresses the equation $\frac{a}{a} * a = a$ for all `a` in `G₀`.
More concisely: For all `a` in a group with identity `G₀`, `a * (a ^^-1) = G₀ ^^-1`, where `^-1` denotes the multiplicative inverse. Therefore, `a * (a * a ^^-1) = a * G₀ ^^-1 = G₀ * a ^^-1 = a`.
|
mul_self_div_self
theorem mul_self_div_self : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] (a : G₀), a * a / a = a
This theorem states that for any value `a` in a group with zero (a mathematical structure that has both multiplication and division operations, and includes a zero element), multiplying `a` by itself and then dividing the result by `a` will always yield `a`. The theorem holds regardless of whether `a` is zero or not.
More concisely: For any group element `a`, the equation `a * a = a * (1 : a → α)` holds, where `1` is the identity element of the group.
|
one_div_ne_zero
theorem one_div_ne_zero : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → 1 / a ≠ 0
This theorem states that for any non-zero element `a` in a Group with Zero structure `G₀`, the reciprocal of `a`, i.e., `1 / a`, is not equal to zero. Here, a Group with Zero `G₀` is a mathematical structure that combines the properties of a group and the existence of a zero element, with the zero element not having a multiplicative inverse.
More concisely: In a Group with Zero structure, the reciprocal of a non-zero element does not equal the zero element.
|
Mathlib.Algebra.GroupWithZero.Basic._auxLemma.9
theorem Mathlib.Algebra.GroupWithZero.Basic._auxLemma.9 :
∀ {M₀ : Type u_2} [inst : CancelMonoidWithZero M₀] {a b c : M₀}, (a * b = a * c) = (b = c ∨ a = 0)
This theorem from the Algebra.GroupWithZero.Basic module in the Mathlib library states that for any type `M₀` that is a Cancel Monoid With Zero, and for any three elements `a`, `b`, and `c` of this type, the statement "`a` multiplied by `b` equals `a` multiplied by `c`" is equivalent to the statement "either `b` equals `c` or `a` equals zero". In other words, if multiplication of `a` with two different elements yields the same result, then either those two elements are the same, or `a` is the zero of the monoid.
More concisely: For any cancel monoid with zero `M₀`, for all `a` in `M₀` and `b, c` in `M₀`, `a * b = a * c` if and only if `b = c` or `a = 0`.
|
eq_zero_of_zero_eq_one
theorem eq_zero_of_zero_eq_one : ∀ {M₀ : Type u_2} [inst : MulZeroOneClass M₀], 0 = 1 → ∀ (a : M₀), a = 0
This theorem states that in a mathematical structure known as a monoid with zero, if zero equals one, then zero is the only element in that monoid. In mathematical terms, for any type `M₀` that has a `MulZeroOneClass` instance (i.e., it is a monoid with zero), if `0 = 1`, then for any element `a` of type `M₀`, `a` must equal `0`.
More concisely: In a monoid with zero, if zero equals one, then every element equals zero.
|
mul_eq_mul_right_iff
theorem mul_eq_mul_right_iff :
∀ {M₀ : Type u_2} [inst : CancelMonoidWithZero M₀] {a b c : M₀}, a * c = b * c ↔ a = b ∨ c = 0
This theorem states that, for a given type `M₀` which is a CancelMonoidWithZero, and for any three elements `a`, `b`, and `c` of this type, the equality `a * c` equals `b * c` is equivalent to `a` equals `b` or `c` equals zero. In other words, if the product of `a` and `c` equals the product of `b` and `c`, then either `a` is equal to `b`, or `c` is zero.
More concisely: For any CancelMonoidWithZero type `M₀` and elements `a`, `b`, and `c` in `M₀`, `a * c = b * c` implies `a = b` or `c = 0`.
|
zero_pow
theorem zero_pow : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {n : ℕ}, n ≠ 0 → 0 ^ n = 0
This theorem states that for any non-zero natural number `n` and for any type `M₀` that is a Monoid with zero (a mathematical structure with a certain set of operations and properties), the nth power of zero is zero. Essentially, it's saying that raising zero to the power of any non-zero natural number will always result in zero, given that our mathematical structure supports such operations.
More concisely: For any monoid with zero `M₀` and natural number `n ≠ 0`, the power `(0 : M₀) ^ n` equals the zero element of `M₀`.
|
mul_right_eq_self₀
theorem mul_right_eq_self₀ : ∀ {M₀ : Type u_2} [inst : CancelMonoidWithZero M₀] {a b : M₀}, a * b = a ↔ b = 1 ∨ a = 0
This theorem, `mul_right_eq_self₀`, states that for any type `M₀`, which forms a cancel monoid with zero, if the product of any two elements `a` and `b` from `M₀` equals `a`, then either `b` is equal to one, or `a` is zero. In other words, if multiplying `a` by `b` doesn't change the value of `a`, it must be because `b` is the multiplicative identity (1), or `a` is the additive identity (0).
More concisely: If `a` and `b` are elements of a cancel monoid `M₀` with zero such that `a * b = a`, then `b = 1` or `a = 0`.
|
Mathlib.Algebra.GroupWithZero.Basic._auxLemma.5
theorem Mathlib.Algebra.GroupWithZero.Basic._auxLemma.5 :
∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {a : M₀} {n : ℕ} [inst_1 : NoZeroDivisors M₀] [inst_2 : Nontrivial M₀],
(a ^ n = 0) = (a = 0 ∧ n ≠ 0)
This theorem, `Mathlib.Algebra.GroupWithZero.Basic._auxLemma.5`, states that for any type `M₀` that is a monoid with zero, given an element `a` of `M₀` and a natural number `n`, and assuming that there are no zero divisors and the domain is nontrivial, `a` raised to the power of `n` equals zero if and only if `a` equals zero and `n` is not zero. In mathematical terms, this is saying that in a monoid with no zero divisors, a power of a number is zero if and only if the base is zero and the exponent is non-zero.
More concisely: In a monoid with no zero divisors and a nontrivial domain, an element raised to the power of a non-zero natural number equals zero if and only if the element is itself zero.
|