CommMonoidWithZero.mul_zero
theorem CommMonoidWithZero.mul_zero : ∀ {M₀ : Type u_4} [self : CommMonoidWithZero M₀] (a : M₀), a * 0 = 0
This theorem states that for any type `M₀` that is a commutative monoid with zero, zero behaves as a right absorbing element under multiplication. In other words, for any element `a` of type `M₀`, the product of `a` and zero is always zero. This is a generalization of the well-known property from number theory which says that any number multiplied by zero results in zero.
More concisely: For any commutative monoid with zero `M₀`, the zero element is a right identity for multiplication, i.e., for all `a` in `M₀`, `a * 0 = 0`.
|
mul_ne_zero_comm
theorem mul_ne_zero_comm :
∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [inst_1 : NoZeroDivisors M₀] {a b : M₀}, a * b ≠ 0 ↔ b * a ≠ 0 := by
sorry
This theorem states that if a type `α` has no zero divisors - that is, no pair of nonzero elements multiplies to zero - then for any two elements `a` and `b` of type `α`, `a * b` is nonzero if and only if `b * a` is also nonzero. In other words, the property of being nonzero is commutative under multiplication in a domain without zero divisors.
More concisely: If `α` is a type without zero divisors, then for all `a, b ∈ α`, `a * b` is nonzero if and only if `b * a` is nonzero.
|
IsRightCancelMulZero.mul_right_cancel_of_ne_zero
theorem IsRightCancelMulZero.mul_right_cancel_of_ne_zero :
∀ {M₀ : Type u} [inst : Mul M₀] [inst_1 : Zero M₀] [self : IsRightCancelMulZero M₀] {a b c : M₀},
b ≠ 0 → a * b = c * b → a = c
This theorem states that in a structure equipped with multiplication and a zero element (i.e., a zero algebraic structure), multiplication by a nonzero element is right cancellative. In other words, for any three elements `a`, `b`, and `c` of this structure, if `b` is not zero and the product of `a` and `b` equals the product of `c` and `b`, then `a` must be equal to `c`. This is a property of multiplication that holds in many mathematical structures, such as the set of integers or real numbers.
More concisely: In a zero algebraic structure, if `a * b = c * b` and `b` is nonzero, then `a = c`.
|
mul_eq_zero
theorem mul_eq_zero :
∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [inst_1 : NoZeroDivisors M₀] {a b : M₀}, a * b = 0 ↔ a = 0 ∨ b = 0 := by
sorry
This theorem states that for any type `M₀`, which is a `MulZeroClass` (a structure that has a multiplication operation and a zero element) and has no zero divisors, the product of any two elements `a` and `b` of `M₀` equals zero if and only if either `a` equals zero, or `b` equals zero. In mathematical terms, we can say that in a ring without zero divisors, the product of two elements is zero if and only if at least one of the elements is zero.
More concisely: In a ring without zero divisors, the product of two non-zero elements is equal to zero if and only if one of them is zero.
|
CommGroupWithZero.mul_inv_cancel
theorem CommGroupWithZero.mul_inv_cancel :
∀ {G₀ : Type u_4} [self : CommGroupWithZero G₀] (a : G₀), a ≠ 0 → a * a⁻¹ = 1
This theorem states that for every nonzero element `a` of a commutative group with zero, denoted `G₀`, the product of `a` and its inverse `a⁻¹` is equal to 1. In other words, any nonzero element of such a group is invertible, and when it is multiplied by its inverse, we get the identity element of the group, which is 1.
More concisely: For every nonzero element `a` in a commutative group `G₀`, `a * a⁻¹ = 1`.
|
mul_ne_zero_iff
theorem mul_ne_zero_iff :
∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [inst_1 : NoZeroDivisors M₀] {a b : M₀}, a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0 := by
sorry
The theorem `mul_ne_zero_iff` states that for any type `M₀` that has a multiplication and zero, and that does not have any zero divisors (NoZeroDivisors), the product of two elements `a` and `b` is not zero if and only if both `a` and `b` are not zero. This theorem essentially formalizes the intuitive notion that in such a structure, zero cannot be produced by multiplying non-zero elements.
More concisely: For types with multiplication and zero without zero divisors, `a * b ≠ 0` if and only if `a ≠ 0` and `b ≠ 0`.
|
mul_self_ne_zero
theorem mul_self_ne_zero :
∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [inst_1 : NoZeroDivisors M₀] {a : M₀}, a * a ≠ 0 ↔ a ≠ 0
This theorem states that for any type `M₀` that has the structure of a multiplication with zero (`MulZeroClass`) and has no zero divisors (`NoZeroDivisors`), an element `a` of `M₀` satisfies the property that `a * a` is not equal to zero if and only if `a` is not equal to zero. In more mathematical terms, for a ring without zero divisors, the square of an element is zero if and only if the element itself is zero.
More concisely: For a ring without zero divisors, an element is non-zero if and only if its square is non-zero.
|
CommGroupWithZero.zpow_neg'
theorem CommGroupWithZero.zpow_neg' :
∀ {G₀ : Type u_4} [self : CommGroupWithZero G₀] (n : ℕ) (a : G₀),
CommGroupWithZero.zpow (Int.negSucc n) a = (CommGroupWithZero.zpow (↑n.succ) a)⁻¹
The theorem `CommGroupWithZero.zpow_neg'` states that for any commutative group with zero `G₀`, any natural number `n`, and any element `a` of `G₀`, the operation of raising `a` to the power of `-(n + 1)` (expressed as `CommGroupWithZero.zpow (Int.negSucc n) a`) is equivalent to the inverse of raising `a` to the power of `(n + 1)` (expressed as `(CommGroupWithZero.zpow (↑n.succ) a)⁻¹`). In other words, for any element of a commutative group with zero, raising it to a negative integer power is the same as taking the reciprocal of the element raised to the corresponding positive integer power.
More concisely: For any commutative group with zero `G₀` and any natural number `n` and element `a` of `G₀`, `CommGroupWithZero.zpow (Int.negSucc n) a` equals the multiplicative inverse of `CommGroupWithZero.zpow (↑n.succ) a`.
|
mul_left_cancel₀
theorem mul_left_cancel₀ :
∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] [inst_2 : IsLeftCancelMulZero M₀] {a b c : M₀},
a ≠ 0 → a * b = a * c → b = c
This theorem states that in a given type `M₀` equipped with multiplication and zero, and also satisfies the left cancellation law for multiplication with zero, if a certain element `a` is not zero, then for any elements `b` and `c`, if the product of `a` and `b` equals the product of `a` and `c`, then `b` must be equal to `c`. This essentially means multiplication by a non-zero element `a` is injective, and hence allows the cancellation of `a` from both sides of the equation `a * b = a * c`.
More concisely: If `a` is a non-zero element in a type `M₀` with multiplication and zero, and `a * b = a * c`, then `b = c`.
|
CommGroupWithZero.inv_zero
theorem CommGroupWithZero.inv_zero : ∀ {G₀ : Type u_4} [self : CommGroupWithZero G₀], 0⁻¹ = 0
This theorem states that in any commutative group with zero (denoted as `CommGroupWithZero`), the inverse of zero is zero itself. In mathematical terms, for any `G₀` of the type `CommGroupWithZero`, the theorem asserts that 0⁻¹ equals 0.
More concisely: In a commutative group with zero, the additive inverse of zero is zero.
|
MulZeroClass.zero_mul
theorem MulZeroClass.zero_mul : ∀ {M₀ : Type u} [self : MulZeroClass M₀] (a : M₀), 0 * a = 0
This theorem states that zero is a left absorbing element for multiplication in any multiplication-zero class. In other words, for any type `M₀` that has a multiplication-zero structure (`MulZeroClass M₀`), the multiplication of zero (`0`) with any element `a` of type `M₀` will always result in zero (`0`). This corresponds to the familiar property in mathematics that anything multiplied by zero is zero.
More concisely: For any type `M₀` with a multiplication-zero structure, multiplication by zero (0) results in zero (0) for all elements of `M₀` (i.e., `∀ (a : M₀), 0 * a = 0`).
|
GroupWithZero.mul_inv_cancel
theorem GroupWithZero.mul_inv_cancel : ∀ {G₀ : Type u} [self : GroupWithZero G₀] (a : G₀), a ≠ 0 → a * a⁻¹ = 1 := by
sorry
This theorem states that for any group with a zero element, if you take any nonzero element `a` from this group, then the product of `a` and its inverse `a⁻¹` is equal to the identity element `1`. In other words, every nonzero element of a group with zero has a multiplicative inverse.
More concisely: For any group with a identity element, every nonzero element has a multiplicative inverse such that the product of an element and its inverse equals the identity element.
|
IsLeftCancelMulZero.mul_left_cancel_of_ne_zero
theorem IsLeftCancelMulZero.mul_left_cancel_of_ne_zero :
∀ {M₀ : Type u} [inst : Mul M₀] [inst_1 : Zero M₀] [self : IsLeftCancelMulZero M₀] {a b c : M₀},
a ≠ 0 → a * b = a * c → b = c
This theorem, called `IsLeftCancelMulZero.mul_left_cancel_of_ne_zero`, states that in any type `M₀` equipped with multiplication and a zero element, if multiplication is left cancellative with respect to zero, then for any three elements `a`, `b`, and `c` of `M₀`, if `a` is not zero and `a * b` equals `a * c`, it necessarily follows that `b` equals `c`. In more mathematical terms, it says that multiplication by a non-zero element is left cancellative.
More concisely: If `M₀` is a type with multiplication and a zero element, and multiplication by a non-zero element is left cancellative, then `a * b = a * c` implies `b = c` for all `a ≠ 0` in `M₀`.
|
MulZeroClass.mul_zero
theorem MulZeroClass.mul_zero : ∀ {M₀ : Type u} [self : MulZeroClass M₀] (a : M₀), a * 0 = 0
This theorem states that zero is a right absorbing element for multiplication in any type that is an instance of the `MulZeroClass`. Formally, for any element `a` of this type, multiplying `a` by zero results in zero, expressed mathematically as `a * 0 = 0`.
More concisely: For any element `a` in a type instancing `MulZeroClass`, `a * 0 = 0`.
|
SemigroupWithZero.mul_zero
theorem SemigroupWithZero.mul_zero : ∀ {S₀ : Type u} [self : SemigroupWithZero S₀] (a : S₀), a * 0 = 0
This theorem states that zero is a right absorbing element for multiplication in any semigroup with zero. In other words, for any semigroup `S₀` with zero and for any element `a` in `S₀`, the result of multiplying `a` with zero is always zero. This property is one of the fundamental characteristics of multiplication in basic number systems like the integers, rational numbers, real numbers, and complex numbers, and is generalized here to any semigroup with zero.
More concisely: In any semigroup with zero, zero is a right identity for multiplication.
|
GroupWithZero.div_eq_mul_inv
theorem GroupWithZero.div_eq_mul_inv : ∀ {G₀ : Type u} [self : GroupWithZero G₀] (a b : G₀), a / b = a * b⁻¹
This theorem, named `GroupWithZero.div_eq_mul_inv`, states that for any type `G₀` that forms a Group with Zero, the division of any two elements `a` and `b` from this group is equivalent to the multiplication of `a` with the multiplicative inverse of `b`. In mathematical terms, it says that `a / b = a * b⁻¹` for any `a` and `b` in `G₀`.
More concisely: For any group with zero `G₀`, the division of two elements `a` and `b` is equivalent to the product of `a` and the multiplicative inverse of `b`: `a / b = a * b⁻¹`.
|
MulZeroOneClass.mul_zero
theorem MulZeroOneClass.mul_zero : ∀ {M₀ : Type u} [self : MulZeroOneClass M₀] (a : M₀), a * 0 = 0
This theorem states that zero is a right absorbing element for multiplication in any type `M₀` that is an instance of the `MulZeroOneClass`. In other words, for any element `a` of type `M₀`, when `a` is multiplied by zero, the result is always zero.
More concisely: For all types `M₀` instance of `MulZeroOneClass` and all elements `a` in `M₀`, `a * 0 = 0`.
|
NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero
theorem NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero :
∀ {M₀ : Type u_4} [inst : Mul M₀] [inst_1 : Zero M₀] [self : NoZeroDivisors M₀] {a b : M₀},
a * b = 0 → a = 0 ∨ b = 0
This theorem states that for any type `M₀` that supports multiplication and has a zero, and does not allow zero divisors, if the product of any two elements `a` and `b` of `M₀` equals zero, then either `a` or `b` must be zero. This is a property that holds in many mathematical structures, such as the integers, where the product of two numbers is zero if and only if at least one of the numbers is zero.
More concisely: In a type `M₀` with multiplication and a zero, without zero divisors, the product of any two non-zero elements is non-zero.
|
MonoidWithZero.zero_mul
theorem MonoidWithZero.zero_mul : ∀ {M₀ : Type u} [self : MonoidWithZero M₀] (a : M₀), 0 * a = 0
This theorem states that zero is a left absorbing element for multiplication in any monoid with zero. Specifically, given any type `M₀` that has a `MonoidWithZero` structure and any element `a` of type `M₀`, the product of zero and `a` will always be zero. In other words, for all `a` in `M₀`, `0 * a = 0`.
More concisely: In any monoid with zero, the multiplicative identity element is zero, i.e., for all elements `a` in the monoid, `0 * a = 0`.
|
mul_left_inj'
theorem mul_left_inj' :
∀ {M₀ : Type u_1} [inst : CancelMonoidWithZero M₀] {a b c : M₀}, c ≠ 0 → (a * c = b * c ↔ a = b)
This theorem states that for any type `M₀`, given that `M₀` is a cancel monoid with zero, for any elements `a`, `b`, and `c` of `M₀`, if `c` is not zero, then `a` multiplied by `c` equals `b` multiplied by `c` if and only if `a` equals `b`. In mathematical terms, this theorem asserts the property of left cancellation in the context of multiplication for types that form a cancel monoid with zero. In essence, if you multiply two elements by the same non-zero element and get equal results, then the original two elements must have been equal.
More concisely: For any cancel monoid with zero `M₀`, if `a`, `b` are in `M₀`, and `c` is non-zero in `M₀`, then `a * c = b * c` implies `a = b`.
|
mul_right_inj'
theorem mul_right_inj' :
∀ {M₀ : Type u_1} [inst : CancelMonoidWithZero M₀] {a b c : M₀}, a ≠ 0 → (a * b = a * c ↔ b = c)
This theorem states that for any type `M₀` which forms a 'Cancel Monoid With Zero', and any elements `a`, `b`, and `c` of this type, if `a` is not zero, then `a` times `b` equals `a` times `c` if and only if `b` equals `c`. In other words, in this type of mathematical structure, multiplication is right-cancellable whenever the left factor is non-zero.
More concisely: For any type `M₀` with a zero element `0` making it a cancel monoid, and for all `a ≠ 0` in `M₀`, `a * b = a * c` if and only if `b = c`.
|
GroupWithZero.inv_zero
theorem GroupWithZero.inv_zero : ∀ {G₀ : Type u} [self : GroupWithZero G₀], 0⁻¹ = 0
This theorem states that in any group with a zero element (denoted as `G₀`), the inverse of `0` is itself `0`. In group theory, this is essentially stating that zero is its own inverse in the group. This is generally true for additive groups, where the inverse of an element is what you add to the element to get the identity (in this case, `0`).
More concisely: In any group with a zero element, the zero element is its own inverse.
|
Mathlib.Algebra.GroupWithZero.Defs._auxLemma.2
theorem Mathlib.Algebra.GroupWithZero.Defs._auxLemma.2 :
∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [inst_1 : NoZeroDivisors M₀] {a b : M₀}, (0 = a * b) = (a = 0 ∨ b = 0)
This theorem, `Mathlib.Algebra.GroupWithZero.Defs._auxLemma.2`, states that for any type `M₀` that has multiplication and zero, and where there are no zero divisors, the equation `0 = a * b` (where `a` and `b` are elements of `M₀`) holds true if and only if either `a` or `b` is zero. In more mathematical terms, for a ring without zero divisors (like the integers or a field like the real numbers), the product of two elements is zero if and only if at least one of the elements is zero.
More concisely: In a ring without zero divisors, the product of two non-zero elements is non-zero. Conversely, the product of two elements is zero if and only if at least one of them is zero.
|
mul_inv_cancel_left₀
theorem mul_inv_cancel_left₀ :
∀ {G₀ : Type u} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → ∀ (b : G₀), a * (a⁻¹ * b) = b
This theorem states that for any type `G₀` that forms a Group with Zero, for any non-zero element `a` of type `G₀`, and for every `b` of type `G₀`, the product of `a` and the product of the inverse of `a` and `b` equals `b`. This is equivalent to cancellation law in the mathematical structure of a group with zero, where if `a` is not zero, then multiplying `a` with the result of multiplying its inverse and another element `b` simplifies back to `b`.
More concisely: For any group with zero `G₀` and non-zero element `a` in `G₀`, `a * (a⁻¹ * b) = b` holds.
|
CommGroupWithZero.zpow_succ'
theorem CommGroupWithZero.zpow_succ' :
∀ {G₀ : Type u_4} [self : CommGroupWithZero G₀] (n : ℕ) (a : G₀),
CommGroupWithZero.zpow (Int.ofNat n.succ) a = CommGroupWithZero.zpow (Int.ofNat n) a * a
The theorem `CommGroupWithZero.zpow_succ'` states that in any commutative group with zero, for any natural number `n` and any element `a` of the group, the power of `a` raised to `(n + 1)` is equal to the power of `a` raised to `n`, times `a` itself i.e., `a ^ (n + 1) = a ^ n * a`. This is essentially the principle of mathematical induction in the context of exponents in a commutative group with zero.
More concisely: In a commutative group with zero, the power of an element raised to the successor of a natural number is equal to the product of the power raised to that natural number and the element itself.
|
CommGroupWithZero.div_eq_mul_inv
theorem CommGroupWithZero.div_eq_mul_inv :
∀ {G₀ : Type u_4} [self : CommGroupWithZero G₀] (a b : G₀), a / b = a * b⁻¹
This theorem states that for any commutative group with zero `G₀` and any elements `a` and `b` of `G₀`, the operation `a / b` is equivalent to `a * b⁻¹`. Here, `b⁻¹` denotes the multiplicative inverse of `b`. In more practical terms, the theorem tells us that division can be expressed as multiplication by the inverse.
More concisely: For any commutative group with zero `G₀` and elements `a, b` in `G₀` with `b ≠ 0`, `a / b` is equivalent to `a * b⁻¹`.
|
CommMonoidWithZero.zero_mul
theorem CommMonoidWithZero.zero_mul : ∀ {M₀ : Type u_4} [self : CommMonoidWithZero M₀] (a : M₀), 0 * a = 0
This theorem states that zero is a left absorbing element for multiplication. Specifically, for any type `M₀` that is a commutative monoid with zero, the multiplication of zero with any element `a` from that type will always result in zero.
More concisely: For any commutative monoid with zero `M₀`, the multiplication of zero with any element `a` in `M₀` results in zero. (i.e., 0 * a = 0 for all a in M₀)
|
mul_eq_zero_comm
theorem mul_eq_zero_comm :
∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [inst_1 : NoZeroDivisors M₀] {a b : M₀}, a * b = 0 ↔ b * a = 0 := by
sorry
The theorem `mul_eq_zero_comm` states that for any type `α` that is a member of the `MulZeroClass` and has no zero divisors (as defined by the `NoZeroDivisors` class), given any two elements `a` and `b` of type `α`, the product `a * b` equals zero if and only if the product `b * a` equals zero. In other words, if the multiplication of two elements `a` and `b` results in zero, then the order of multiplication does not matter; the multiplication of `b` and `a` will also yield zero, and vice versa. This theorem reflects the commutative property of multiplication in a ring without zero divisors.
More concisely: For types `α` in `MulZeroClass` with no zero divisors, `a * b = 0` if and only if `b * a = 0`.
|
GroupWithZero.zpow_succ'
theorem GroupWithZero.zpow_succ' :
∀ {G₀ : Type u} [self : GroupWithZero G₀] (n : ℕ) (a : G₀),
GroupWithZero.zpow (Int.ofNat n.succ) a = GroupWithZero.zpow (Int.ofNat n) a * a
This theorem states that for any given group with zero (denoted by G₀), and for any element 'a' of G₀ and natural number 'n', the power operation of 'a' raised to the integer value of ('n' + 1) is equivalent to the power operation of 'a' raised to the integer value of 'n' multiplied by 'a'. In mathematical terms, this can be expressed as `a ^ (n + 1) = a ^ n * a`, where '^' represents the power operation.
More concisely: For any group with zero 'G₀', and for any 'a' in 'G₀' and natural number 'n', the power 'a ^ (n + 1)' equals 'a ^ n' multiplied by 'a'.
|
mul_right_injective₀
theorem mul_right_injective₀ :
∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] [inst_2 : IsLeftCancelMulZero M₀] {a : M₀},
a ≠ 0 → Function.Injective fun x => a * x
The theorem `mul_right_injective₀` states that for any type `M₀` that has a multiplication operation and zero and satisfies the property of left cancellation for multiplication with zero, if `a` is a non-zero element of `M₀`, then the function which maps each element `x` to the product of `a` and `x` is injective. In other words, if `a` times `x` equals `a` times `y`, then `x` must equal `y`.
More concisely: If `M₀` is a type with multiplication and zero, and `a` is a non-zero element with left cancellation property, then the function `x ↦ a * x` is injective on `M₀`.
|
mul_eq_zero_of_left
theorem mul_eq_zero_of_left : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] {a : M₀}, a = 0 → ∀ (b : M₀), a * b = 0 := by
sorry
This theorem, `mul_eq_zero_of_left`, establishes the rule for multiplication with zero in a `MulZeroClass`. Given any type `M₀` that is a multiplication-zero class (i.e., a set with an operation of multiplication that obeys certain laws and contains an element, 0, that when multiplied with any other element results in 0), the theorem states that if any element `a` is equal to zero, then the product of `a` and any other element `b` is also zero. In simpler words, multiplying by zero always yields zero in a multiplication-zero class.
More concisely: In a multiplication-zero class, multiplying any element by zero results in zero.
|
zero_eq_mul
theorem zero_eq_mul :
∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [inst_1 : NoZeroDivisors M₀] {a b : M₀}, 0 = a * b ↔ a = 0 ∨ b = 0 := by
sorry
This theorem states that for any type `M₀` that is a multiplication zero class (a structure with multiplication, zero, and a rule that any number times zero equals zero) and has no zero divisors (meaning that the only way to get zero by multiplying two numbers together is if one or both of them is zero), the equality between zero and the product of two elements `a` and `b` from `M₀` is equivalent to either `a` or `b` being zero. In mathematical terms, for any `a` and `b` in a multiplication zero class with no zero divisors, the statement `0 = a * b` is true if and only if `a = 0` or `b = 0`.
More concisely: In a multiplication zero class without zero divisors, the product of two non-zero elements is zero if and only if one of them is zero.
|
GroupWithZero.zpow_zero'
theorem GroupWithZero.zpow_zero' : ∀ {G₀ : Type u} [self : GroupWithZero G₀] (a : G₀), GroupWithZero.zpow 0 a = 1 := by
sorry
This theorem states that for any element `a` from a group with a zero element (denoted as `G₀`), raising `a` to the power of zero gives the identity element of the group, specifically `1`. In other words, regardless of what `a` is, `a` raised to the power of zero is always `1`. This is formally written as `a ^ 0 = 1`.
More concisely: In any group with a zero element, raising any group element to the power of zero yields the identity element. Equivalently, for all group elements `a`, `a^0 = 1`.
|
mul_left_injective₀
theorem mul_left_injective₀ :
∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] [inst_2 : IsRightCancelMulZero M₀] {b : M₀},
b ≠ 0 → Function.Injective fun a => a * b
The theorem `mul_left_injective₀` states that for any type `M₀` equipped with a multiplication operation, a zero element, and a property that right multiplication by zero is cancelable, for any non-zero element `b` of type `M₀`, the function that multiplies an element `a` of `M₀` by `b` is injective. In other words, in such a mathematical structure, if `a * b = c * b` then `a = c` whenever `b` is not zero.
More concisely: For any type `M₀` with multiplication, zero, and right zero-cancelation, the function `(× b) : M₀ → M₀` is injective, where `b` is a non-zero element.
|
mul_right_cancel₀
theorem mul_right_cancel₀ :
∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] [inst_2 : IsRightCancelMulZero M₀] {a b c : M₀},
b ≠ 0 → a * b = c * b → a = c
This theorem states that for any type `M₀` endowed with multiplication and a zero element, and where multiplication by zero on the right side cancels out any non-zero values, given three elements `a`, `b`, and `c` of `M₀`, if `b` is not equal to zero and the product of `a` and `b` is equal to the product of `c` and `b`, then `a` must be equal to `c`. This is a form of the "cancellation law" for multiplication.
More concisely: If `M₀` is a type with multiplication and zero such that `a * b = c * b` implies `a = c` for all non-zero `b` in `M₀`, then `M₀` satisfies the left cancellation law for multiplication.
|
mul_self_eq_zero
theorem mul_self_eq_zero :
∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [inst_1 : NoZeroDivisors M₀] {a : M₀}, a * a = 0 ↔ a = 0
This theorem states that for any type `M₀` which has a multiplication operation that includes a zero element, and where zero divisors are not allowed, a product of any element `a` with itself (`a * a`) equals zero if and only if `a` is zero. In more traditional mathematical notation, this theorem is saying that for all `a` in some multiplication zero class `M₀`, `a^2 = 0` if and only if `a = 0`.
More concisely: For any type `M₀` with multiplication and a zero element, without zero divisors, `a * a = 0` if and only if `a = 0`.
|
Mathlib.Algebra.GroupWithZero.Defs._auxLemma.1
theorem Mathlib.Algebra.GroupWithZero.Defs._auxLemma.1 :
∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [inst_1 : NoZeroDivisors M₀] {a b : M₀}, (a * b = 0) = (a = 0 ∨ b = 0)
This theorem, from the Mathlib Algebra GroupWithZero Definitions, states that for any type `M₀` that is a multiplication zero class and has no zero divisors, and for any two elements `a` and `b` of type `M₀`, the condition that the product `a * b` equals zero is equivalent to either `a` equals zero or `b` equals zero. This is essentially a formalization of the standard mathematical property that in a domain (a ring without zero divisors), the product of two elements equals zero if and only if one of the elements is zero.
More concisely: In a multiplication zero class `M₀` without zero divisors, `a * b = 0` if and only if `a = 0` or `b = 0`.
|
MonoidWithZero.mul_zero
theorem MonoidWithZero.mul_zero : ∀ {M₀ : Type u} [self : MonoidWithZero M₀] (a : M₀), a * 0 = 0
This theorem states that zero is a right absorbing element for the multiplication operation in any MonoidWithZero. Formally, for any type `M₀` that has a MonoidWithZero structure and for any element `a` of type `M₀`, the result of multiplying `a` with zero is always zero. In the language of mathematics, this can be stated as "for all `a` in `M₀`, `a * 0 = 0`".
More concisely: In any MonoidWithZero type `M₀`, the multiplication of any element `a` with zero is zero, i.e., `a * 0 = 0`.
|
MulZeroOneClass.zero_mul
theorem MulZeroOneClass.zero_mul : ∀ {M₀ : Type u} [self : MulZeroOneClass M₀] (a : M₀), 0 * a = 0
This theorem asserts that zero acts as a left absorbing element for multiplication in a multiplication-zero-one structure (MulZeroOneClass). Specifically, for any element `a` of type `M₀`, the product of zero and `a` (0 * a) is always zero. This is a generalized version of the familiar arithmetic property that multiplying any number by zero results in zero.
More concisely: In a multiplication-zero-one structure, the multiplication of any element with zero is equal to zero.
|
SemigroupWithZero.zero_mul
theorem SemigroupWithZero.zero_mul : ∀ {S₀ : Type u} [self : SemigroupWithZero S₀] (a : S₀), 0 * a = 0
This theorem states that zero is a left absorbing element for the multiplication operation in a semigroup with zero. In other words, for any type `S₀` that forms a semigroup with zero, when zero is multiplied with any element `a` from `S₀`, the result is always zero.
More concisely: In a semigroup with zero, the multiplication of any element with zero results in zero.
|
mul_eq_zero_of_right
theorem mul_eq_zero_of_right : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] (a : M₀) {b : M₀}, b = 0 → a * b = 0 := by
sorry
This theorem, `mul_eq_zero_of_right`, states that for any type `M₀` that has a multiplication and zero operation (`MulZeroClass`), given any element `a` of `M₀` and any other element `b` of `M₀`, if `b` is equal to zero, then the product of `a` and `b` is also zero. Essentially, it captures the common mathematical property that anything multiplied by zero equals zero, specified in the context of a right multiplication.
More concisely: For any type `M₀` with multiplication and zero (`MulZeroClass`) and any elements `a` and `b` in `M₀`, if `b = 0`, then `a * b = 0`.
|
mul_inv_cancel
theorem mul_inv_cancel : ∀ {G₀ : Type u} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → a * a⁻¹ = 1
This theorem states that for any non-zero element 'a' of a group with zero 'G₀', the product of 'a' and its multiplicative inverse 'a⁻¹' equals one. This is essentially saying that the multiplicative inverse property holds in a group with zero, where any element times its inverse equals the identity element, which is one in this context.
More concisely: For any non-zero element 'a' in a group G with identity element G₀, a * a⁻¹ = G₀.
|
CommGroupWithZero.zpow_zero'
theorem CommGroupWithZero.zpow_zero' :
∀ {G₀ : Type u_4} [self : CommGroupWithZero G₀] (a : G₀), CommGroupWithZero.zpow 0 a = 1
This theorem states that for any element `a` in a commutative group with zero (`CommGroupWithZero G₀`), the zero-th power of `a` (denoted `a ^ 0` or `CommGroupWithZero.zpow 0 a` in Lean 4) is equal to the identity element of the group, `1`. This is a generalization of the well-known rule in arithmetic that any number raised to the power of zero equals one, extended to the abstract setting of commutative groups with zero.
More concisely: For any commutative group with zero `G`, the zero-th power of any element `a` in `G` equals the group identity `1` (` CommGroupWithZero.zpow 0 a = 1`).
|
mul_inv_cancel_right₀
theorem mul_inv_cancel_right₀ :
∀ {G₀ : Type u} [inst : GroupWithZero G₀] {b : G₀}, b ≠ 0 → ∀ (a : G₀), a * b * b⁻¹ = a
This theorem states that for any type `G₀` that forms a group with zero, given any non-zero element `b` of `G₀` and any other element `a` of `G₀`, the formula `a * b * b⁻¹` simplifies to `a`. Here, `b⁻¹` denotes the multiplicative inverse of `b`. This is a property of groups where multiplying an element by its inverse results in the identity, thereby canceling the effect of `b` and `b⁻¹` in the multiplication.
More concisely: In any group with an identity element, for all `a, b` in the group with `b` non-zero, `a * b * b⁻¹ = a`.
|
GroupWithZero.zpow_neg'
theorem GroupWithZero.zpow_neg' :
∀ {G₀ : Type u} [self : GroupWithZero G₀] (n : ℕ) (a : G₀),
GroupWithZero.zpow (Int.negSucc n) a = (GroupWithZero.zpow (↑n.succ) a)⁻¹
This theorem states that for any type `G₀` which forms a group with an additional distinguished element `0`, and for any natural number `n` and element `a` of `G₀`, the power function `zpow` applied to the negative successor of `n` (i.e., `-(n + 1)`) and `a` is equal to the inverse of the power function applied to the successor of `n` (i.e., `n + 1`) and `a`. In other words, raising `a` to the power of `-(n + 1)` is the same as taking the inverse of `a` raised to the power of `n + 1`. This is captured mathematically as `a ^ -(n + 1) = (a ^ (n + 1))⁻¹`.
More concisely: For any group `G₀` with identity element `0`, and for all natural numbers `n` and elements `a` in `G₀`, `a ^ (-(n + 1)) = (a ^ (n + 1))⁻¹`.
|