IsLeftRegular.subsingleton
theorem IsLeftRegular.subsingleton : ∀ {R : Type u_1} [inst : MulZeroClass R], IsLeftRegular 0 → Subsingleton R := by
sorry
The theorem `IsLeftRegular.subsingleton` states that for any type `R` equipped with a multiplication operation that also has a zero element (`MulZeroClass R`), the element `0` is left-regular if and only if `R` is a singleton set (i.e., `R` is trivial). In other words, the property of `0` being left-regular, which means that multiplication on the left by `0` is a function that never maps different elements to the same element, is equivalent to the condition that `R` contains at most one element.
More concisely: The element 0 of a type equipped with multiplication and a zero element is left-regular if and only if the type is a singleton.
|
IsLeftRegular.ne_zero
theorem IsLeftRegular.ne_zero :
∀ {R : Type u_1} [inst : MulZeroClass R] {a : R} [inst_1 : Nontrivial R], IsLeftRegular a → a ≠ 0
This theorem states that for any type `R` that has a multiplication operation and a zero element (`MulZeroClass`), as well as a nontrivial element, if an element `a` of `R` is a left-regular element (i.e., multiplication on the left by `a` is injective), then `a` cannot be the zero element. In more mathematical terms, if a non-zero element of a nonzero ring has the property that multiplication on the left by this element is injective, then this element is non-zero.
More concisely: If `R` is a non-zero ring and `a` is a left-regular element of `R` (i.e., `x ≠ 0 → a * x ≠ a`), then `a ≠ 0`.
|
IsAddLeftRegular.add
theorem IsAddLeftRegular.add :
∀ {R : Type u_1} [inst : AddSemigroup R] {a b : R},
IsAddLeftRegular a → IsAddLeftRegular b → IsAddLeftRegular (a + b)
In an additive semigroup, this theorem states that if you have two elements, `a` and `b`, that are add-left-regular (meaning that adding each of these elements to any other element on the left is an injective operation), then the sum of `a` and `b` is also add-left-regular. In other words, in any additive semigroup, the property of being add-left-regular is preserved under addition.
More concisely: In an additive semigroup, if `a` and `b` are add-left-regular elements, then `a + b` is also add-left-regular.
|
mul_isLeftRegular_iff
theorem mul_isLeftRegular_iff :
∀ {R : Type u_1} [inst : Semigroup R] {a : R} (b : R),
IsLeftRegular a → (IsLeftRegular (a * b) ↔ IsLeftRegular b)
This theorem states that for any semigroup `R` and any element `a` in `R`, if `a` is left-regular, then another element `b` in `R` is left-regular if and only if the product `a * b` is left-regular. Here, an element is termed "left-regular" if multiplying any other element by it on the left yields a unique result, i.e., the mapping defined by left multiplication is injective. In other words, a left-regular element preserves the left-regularity of other elements upon multiplication.
More concisely: For any semigroup R and any of its elements a, if a is left-regular then two elements a and b are left-regular if and only if their product a * b is left-regular.
|
IsAddUnit.isAddRegular
theorem IsAddUnit.isAddRegular : ∀ {R : Type u_1} [inst : AddMonoid R] {a : R}, IsAddUnit a → IsAddRegular a
This theorem states that if an element 'a' in an additive monoid 'R' is an additive unit, then 'a' is add-regular. Here, an element being an additive unit means it has a two-sided additive inverse. Moreover, 'a' being add-regular refers to the property that if 'a' plus any element 'b' is equal to 'a' plus another element 'c', then 'b' must be equal to 'c' (and similarly for addition on the other side). The theorem holds for any additive monoid 'R'.
More concisely: If an additive unit 'a' in an additive monoid 'R' is add-regular, then it is a two-sided cancellation element.
|
isRegular_of_ne_zero
theorem isRegular_of_ne_zero : ∀ {R : Type u_1} [inst : CancelMonoidWithZero R] {a : R}, a ≠ 0 → IsRegular a
This theorem states that in any integral domain, all non-zero elements are regular. More specifically, for any type `R` equipped with a `CancelMonoidWithZero` structure (which is a mathematical structure combining properties of a monoid and a total order where cancellation laws hold and an element 0 has special properties) and any element `a` of type `R`, if `a` is not equal to 0, then `a` is a regular element. Here, a regular element of a ring is one where multiplication by that element, on either side, is injective.
More concisely: In any integral domain, every non-zero element is a regular multiplicative element.
|
IsLeftRegular.of_mul
theorem IsLeftRegular.of_mul :
∀ {R : Type u_1} [inst : Semigroup R] {a b : R}, IsLeftRegular (a * b) → IsLeftRegular b
The theorem `IsLeftRegular.of_mul` states that for any semigroup `R`, and any elements `a` and `b` from that semigroup, if `b` becomes a left-regular element after being multiplied on the left by a left-regular element `a`, then `b` itself is a left-regular element. Here, a left-regular element refers to an element `c` such that the function that multiplies `c` on the left to any given element is injective, meaning that it preserves distinctness of elements in the semigroup.
More concisely: If `a` is a left-regular element in semigroup `R` and left multiplying `b` by `a` results in a left-regular element, then `b` is a left-regular element in `R`.
|
isAddRightRegular_of_add_eq_zero
theorem isAddRightRegular_of_add_eq_zero :
∀ {R : Type u_1} [inst : AddMonoid R] {a b : R}, a + b = 0 → IsAddRightRegular a
This theorem states that for any type `R` that has an addition operator (forming an additive monoid), if there exist two elements `a` and `b` in `R` such that their sum equals zero (i.e., `a + b = 0`), then the element `a` is an add-right-regular element. In other words, adding `a` to any other element on the right is an injective operation, which means that if `x + a = y + a`, then `x` must equal `y`.
More concisely: If `R` is an additive monoid with zero `z`, and `a, b` are elements of `R` with `a + b = z`, then `a` is right-cancelable (i.e., for all `x, y` in `R`, `x + a = y + a` implies `x = y`).
|
IsLeftRegular.all
theorem IsLeftRegular.all : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : IsLeftCancelMul R] (g : R), IsLeftRegular g := by
sorry
The theorem `IsLeftRegular.all` states that if in a multiplication structure `R`, every multiplication operation cancels on the left (i.e., for all `a`, `b`, and `c` in `R`, if `a * b = a * c` then `b = c`), then every element `g` of `R` is left-regular. In the context of this theorem, an element is said to be left-regular if multiplication on the left by this element is an injective function, meaning that if `g * x = g * y`, then `x = y`.
More concisely: In a multiplication structure where every multiplication is left-cancellative, every element is left-invertible.
|
IsRegular.left
theorem IsRegular.left : ∀ {R : Type u_1} [inst : Mul R] {c : R}, IsRegular c → IsLeftRegular c
The theorem `IsRegular.left` states that for any type `R` that has a multiplication operation (denoted by `Mul R`), if an element `c` of `R` is a regular element (which means that both multiplication on the left and right by `c` are injective), then `c` is a left-regular element. In other words, multiplication on the left by `c` is injective. This is usually expressed in the mathematical form as: if for any two elements `a` and `b` from `R`, `c*a = c*b` implies `a = b`, then `c` is a left-regular element.
More concisely: If `c` is a regular element in a type `R` with multiplication, then `c` being left-multiplicatively injective (i.e., `c * a = c * b` implies `a = b`) is a consequence of `c`'s regularity.
|
isRegular_mul_iff
theorem isRegular_mul_iff :
∀ {R : Type u_1} [inst : CommSemigroup R] {a b : R}, IsRegular (a * b) ↔ IsRegular a ∧ IsRegular b
This theorem states that in any commutative semigroup `R`, a product `a * b` is regular if and only if both factors `a` and `b` are regular. Regular elements in a semigroup are those for which there exists a unique solution to the equation `axa = a` for any `x` in the semigroup. The theorem, hence, relates the regularity of a product to the regularity of its factors.
More concisely: In a commutative semigroup, an element `a * b` is regular if and only if both factors `a` and `b` are regular.
|
add_isAddLeftRegular_iff
theorem add_isAddLeftRegular_iff :
∀ {R : Type u_1} [inst : AddSemigroup R] {a : R} (b : R),
IsAddLeftRegular a → (IsAddLeftRegular (a + b) ↔ IsAddLeftRegular b)
This theorem states that for any type `R` that forms an additive semigroup, and for any elements `a` and `b` of `R`, if `a` is an add-left-regular element (meaning that adding `a` to any other element from the left yields a unique result), then adding `b` to `a` on the left is also an add-left-regular element if and only if `b` itself is an add-left-regular element. In mathematical terms, if addition on the left by `a` is injective, then addition on the left by `a+b` is also injective if and only if addition on the left by `b` is injective.
More concisely: For any additive semigroup `R` and add-left-regular elements `a` and `b` in `R`, `a` is add-left-regular if and only if `a + b` is add-left-regular if and only if `b` is add-left-regular.
|
not_isLeftRegular_zero
theorem not_isLeftRegular_zero : ∀ {R : Type u_1} [inst : MulZeroClass R] [nR : Nontrivial R], ¬IsLeftRegular 0 := by
sorry
The theorem `not_isLeftRegular_zero` states that in a non-trivial ring (a ring that has at least two distinct elements), the element `0` is not left-regular. Here, an element is considered left-regular if multiplication on the left by this element is an injective function, meaning that if `c * x = c * y`, then `x = y`. However, for the element `0` in a non-trivial ring, this property does not hold.
More concisely: In a non-trivial ring, the element 0 is not left-regular.
|
isRightRegular_of_mul_eq_one
theorem isRightRegular_of_mul_eq_one : ∀ {R : Type u_1} [inst : Monoid R] {a b : R}, a * b = 1 → IsRightRegular a := by
sorry
This theorem states that in any monoid `R`, if an element `a` multiplies with another element `b` to give the identity element `1`, then `a` is a right-regular element. In other words, for any two elements `x` and `y` in the monoid, if `x * a = y * a` then `x = y`. This corresponds to the property that the operation of multiplying by `a` on the right is injective.
More concisely: In a monoid, if for all elements `x` and `y`, `x * a = y * a` implies `x = y`, then `a` is a right-regular element.
|
IsRightRegular.subsingleton
theorem IsRightRegular.subsingleton : ∀ {R : Type u_1} [inst : MulZeroClass R], IsRightRegular 0 → Subsingleton R := by
sorry
The theorem `IsRightRegular.subsingleton` states that for any type `R` equipped with a multiplication operation that also identifies zero, the element `0` is right-regular if and only if `R` is a trivial or singleton set. In other words, multiplication on the right by `0` is injective (where each input is mapped to a unique output) if and only if `R` has at most one element.
More concisely: The element 0 is right-regular in a type equipped with multiplication and identifies zero if and only if the type is trivial or has at most one element.
|
isAddRegular_zero
theorem isAddRegular_zero : ∀ {R : Type u_1} [inst : AddZeroClass R], IsAddRegular 0
The theorem `isAddRegular_zero` states that for any type `R` that has an addition operation and a zero element (i.e., it is an `AddZeroClass`), zero is an additive regular element. An additive regular element is an element that when added to another element, results in a unique solution. In other words, if adding zero to any element on either side doesn't change the element, then zero is an additive regular element.
More concisely: For any `AddZeroClass` type `R`, the zero element is an additive identity, meaning that for all `x` in `R`, `x + 0 = x` and `0 + x = x`.
|
IsRightRegular.ne_zero
theorem IsRightRegular.ne_zero :
∀ {R : Type u_1} [inst : MulZeroClass R] {a : R} [inst_1 : Nontrivial R], IsRightRegular a → a ≠ 0
This theorem states that for any type `R` that has multiplication and zero, and is nontrivial (i.e., there exist at least two distinct elements), if an element `a` from `R` is right-regular (meaning that multiplication by `a` from the right is an injective function), then `a` cannot be zero. In other words, no right-regular element of a nontrivial multiplication-zero class can be zero.
More concisely: If type `R` has multiplication and zero, and `a` is a right-regular element of `R` in a nontrivial multiplication-zero class, then `a` is not equal to zero.
|
isLeftRegular_of_mul_eq_one
theorem isLeftRegular_of_mul_eq_one : ∀ {R : Type u_1} [inst : Monoid R] {a b : R}, b * a = 1 → IsLeftRegular a := by
sorry
The theorem `isLeftRegular_of_mul_eq_one` states that for any type `R` that forms a monoid (denoted by `Monoid R`), if there are two elements `a` and `b` in `R` such that the multiplication of `b` and `a` yields the monoid's identity element (`b * a = 1`), then `a` is a left-regular element. In mathematical terms, if `b * a = 1` for some elements `a` and `b` in a monoid, then the function defined by left-multiplication by `a` is injective.
More concisely: If `b * a = 1` in a monoid `R`, then `a` is a left-regular element, i.e., the left-multiplication by `a` is an injection.
|
IsLeftRegular.right_of_commute
theorem IsLeftRegular.right_of_commute :
∀ {R : Type u_1} [inst : Mul R] {a : R}, (∀ (b : R), Commute a b) → IsLeftRegular a → IsRightRegular a
This theorem states that for any type `R` equipped with a multiplication operation, if an element `a` of this type commutes with all other elements (that is, for any element `b` from `R`, `a * b = b * a`), and `a` is a left-regular element (meaning that multiplication on the left by `a` is injective), then `a` is also a right-regular element (meaning that multiplication on the right by `a` is also injective).
More concisely: If `a` is an element of a commutative ring `R` that commutes with all elements and is left-regular, then `a` is right-regular.
|
IsAddRightRegular.add
theorem IsAddRightRegular.add :
∀ {R : Type u_1} [inst : AddSemigroup R] {a b : R},
IsAddRightRegular a → IsAddRightRegular b → IsAddRightRegular (a + b)
The theorem states that in an additive semigroup, if two elements 'a' and 'b' have the property that adding them on the right to any other element is an injective function, then their sum also has this property. In other words, if 'a' and 'b' are add-right-regular elements in an additive semigroup, then their sum 'a + b' is also an add-right-regular element. This means that if we have two elements 'a' and 'b' such that adding 'a' or 'b' to any element 'x' with 'x + a' or 'x + b' gives unique results, then adding 'a + b' to any element 'x' with 'x + (a + b)' will also yield unique results.
More concisely: If 'a' and 'b' are add-right-regular elements in an additive semigroup, then their sum 'a + b' is also an add-right-regular element.
|
IsRegular.right
theorem IsRegular.right : ∀ {R : Type u_1} [inst : Mul R] {c : R}, IsRegular c → IsRightRegular c
The theorem `IsRegular.right` states that for any type `R` that has a multiplication operation and for any element `c` of `R`, if `c` is a regular element (i.e., both left-multiplication and right-multiplication by `c` are injective), then `c` is also a right-regular element (i.e., right-multiplication by `c` is injective). This implies that if an element preserves distinctness when it multiplies other elements from either left or right, it also preserves distinctness when it multiplies other elements from the right.
More concisely: If an element in a ring is regular (i.e., both left and right multiplications by it are injective), then it is right-regular (i.e., right multiplication by it is injective).
|
isAddLeftRegular_of_add_eq_zero
theorem isAddLeftRegular_of_add_eq_zero :
∀ {R : Type u_1} [inst : AddMonoid R] {a b : R}, b + a = 0 → IsAddLeftRegular a
This theorem states that for any type `R` that is an additive monoid, if for elements `a` and `b` of `R`, the sum of `b` and `a` equals zero, then `a` is an add-left-regular element. An add-left-regular element is defined as an element `c` such that adding `c` to any other element on the left is an injective function, which means that for every distinct pair of elements, their sums with `c` on the left are also distinct.
More concisely: If `R` is an additive monoid and `a` and `b` are elements of `R` such that `a + b = 0`, then `a` is an add-left-regular element.
|
IsRightRegular.of_mul
theorem IsRightRegular.of_mul :
∀ {R : Type u_1} [inst : Semigroup R] {a b : R}, IsRightRegular (b * a) → IsRightRegular b
The theorem `IsRightRegular.of_mul` states that, for any type `R` that forms a semigroup under multiplication, given elements `a` and `b` of `R`, if `b` multiplied on the right by `a` is a right-regular element (meaning that multiplication on the right by `b * a` is an injective operation), then `b` itself is right-regular. This means that multiplying any element of `R` on the right by `b` yields a unique result, with no two different elements of `R` giving the same product when multiplied by `b`.
More concisely: If `b * a` is right-regular in a semigroup `R`, then `b` is right-regular.
|
IsRightRegular.all
theorem IsRightRegular.all : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : IsRightCancelMul R] (g : R), IsRightRegular g
The theorem `IsRightRegular.all` asserts that in any type `R` with a multiplication operation where right cancellation is always guaranteed, every element `g` of `R` is a right-regular element. In other words, if for any elements `a, b, c` of `R`, the equality `a*c = b*c` always implies `a = b`, then for every `g` in `R`, the function that multiplies `g` on the right is injective, i.e., for any `x, y` in `R`, if `x*g = y*g` then `x = y`.
More concisely: If every element in a type `R` with right cancellation for multiplication has right-multiplication by a fixed element `g` defined as a function, then this function is injective.
|
isRegular_iff_ne_zero
theorem isRegular_iff_ne_zero :
∀ {R : Type u_1} [inst : CancelMonoidWithZero R] {a : R} [inst_1 : Nontrivial R], IsRegular a ↔ a ≠ 0
This theorem states that in a non-trivial integral domain, an element is regular if and only if it is not zero. Here, the term "integral domain" refers to a specific type of mathematical structure (denoted as `R` in the theorem) that behaves similarly to the integers in terms of arithmetic operations. A "non-trivial" integral domain implies that there is at least one element other than zero. A regular element is one that can be cancelled from both sides of an equation without altering the equality.
More concisely: In a non-trivial integral domain, an element is regular if and only if it is non-zero.
|
not_isRightRegular_zero
theorem not_isRightRegular_zero : ∀ {R : Type u_1} [inst : MulZeroClass R] [nR : Nontrivial R], ¬IsRightRegular 0 := by
sorry
This theorem states that in a non-trivial ring, the zero element is not right-regular. In other words, multiplication on the right by zero is not injective. This is true because in any ring, multiplying any element by zero always results in zero, thus failing the condition for injectivity which requires each input to map to a unique output. The condition of the ring being non-trivial ensures that there is at least one element in the ring that is not zero.
More concisely: In a non-trivial ring, multiplication by the additive identity is not an injection.
|
IsRegular.and_of_mul_of_mul
theorem IsRegular.and_of_mul_of_mul :
∀ {R : Type u_1} [inst : Semigroup R] {a b : R},
IsRegular (a * b) → IsRegular (b * a) → IsRegular a ∧ IsRegular b
This theorem, `IsRegular.and_of_mul_of_mul`, states that for any semigroup `R` and any elements `a` and `b` from `R`, if the product `a * b` and the product `b * a` are both regular, then `a` and `b` are also regular. Here, regularity is a property of an element in algebra, specifically in ring theory, where an element `a` is regular if there exist a `b` such that `a * b * a = a`.
More concisely: If `a * b` and `b * a` are regular elements in a semigroup `R`, then `a` and `b` are regular in `R`.
|
isAddRegular_add_iff
theorem isAddRegular_add_iff :
∀ {R : Type u_1} [inst : AddCommSemigroup R] {a b : R}, IsAddRegular (a + b) ↔ IsAddRegular a ∧ IsAddRegular b := by
sorry
This theorem states that in any additive commutative semigroup, a sum is add-regular if and only if its summands are add-regular. In simpler terms, in a context where addition is both associative and commutative, if the sum of two elements has the property that adding it with another element and getting the same result implies the other element was also the same (which is the definition of add-regular), this is equivalent to both elements individually having this property.
More concisely: In an additive commutative semigroup, an element is add-regular if and only if its summands are add-regular.
|
IsAddRegular.and_of_add_of_add
theorem IsAddRegular.and_of_add_of_add :
∀ {R : Type u_1} [inst : AddSemigroup R] {a b : R},
IsAddRegular (a + b) → IsAddRegular (b + a) → IsAddRegular a ∧ IsAddRegular b
This theorem, `IsAddRegular.and_of_add_of_add`, states that for any type `R` that forms an additive semigroup, and for any two elements `a` and `b` from this type, if both `a + b` and `b + a` are regular under addition (meaning that for all `x` and `y` in `R`, `a + b + x = a + b + y` implies `x = y` and similarly for `b + a`), then `a` and `b` themselves are also regular under addition. The theorem is a more commonly used implication of a property called `add_and_add_iff`, and it splits its hypotheses into two separate conditions, instead of linking them with a logical `and` (`∧`).
More concisely: If `a` and `b` are elements of an additive semigroup `R` such that `a + b` and `b + a` are regular under addition, then `a` and `b` are also regular under addition.
|
IsUnit.isRegular
theorem IsUnit.isRegular : ∀ {R : Type u_1} [inst : Monoid R] {a : R}, IsUnit a → IsRegular a
The theorem `IsUnit.isRegular` states that for any type `R` that forms a monoid, if an element `a` of `R` is a unit, then `a` is regular. In other words, in the context of a monoid, any element that has a two-sided inverse (a unit) also satisfies the property of regularity.
More concisely: In a monoid, every unit is regular.
|
add_isAddRightRegular_iff
theorem add_isAddRightRegular_iff :
∀ {R : Type u_1} [inst : AddSemigroup R] {a : R} (b : R),
IsAddRightRegular a → (IsAddRightRegular (b + a) ↔ IsAddRightRegular b)
In the context of a type `R` equipped with an addition operation (i.e., an `AddSemigroup`), an element `a` of `R` is called "add-right-regular" if and only if the function that adds `a` on the right to any element is injective. The theorem states that for any such element `a` and for any element `b` of `R`, if `a` is add-right-regular, then `b` is add-right-regular if and only if the element obtained by adding `a` to `b` is add-right-regular. In other words, adding an add-right-regular element on the right preserves the property of being add-right-regular.
More concisely: If `a` is an add-right-regular element in an `AddSemigroup` `R`, then `b` is add-right-regular if and only if `a + b` is add-right-regular.
|
IsAddRegular.left
theorem IsAddRegular.left : ∀ {R : Type u_2} [inst : Add R] {c : R}, IsAddRegular c → IsAddLeftRegular c
The theorem states that for any type `R` that has an addition operation, if an element `c` of `R` is add-regular (i.e., addition by `c` on either side is injective), then `c` is also add-left-regular (i.e., adding `c` to other elements on the left is an injective function). This means that for any two elements in `R`, if `c + x = c + y` implies `x = y`, then `c` is an add-regular element.
More concisely: If `R` is a type with additions, and `c` is an add-regular element (i.e., `x + c = y + c` implies `x = y`), then `c` is add-left-regular (i.e., `x = y` whenever `x = c + z` and `y = c + w`).
|
IsLeftRegular.mul
theorem IsLeftRegular.mul :
∀ {R : Type u_1} [inst : Semigroup R] {a b : R}, IsLeftRegular a → IsLeftRegular b → IsLeftRegular (a * b) := by
sorry
In a semigroup structure, the theorem `IsLeftRegular.mul` states that for any given type `R` equipped with a semigroup structure and any two elements `a` and `b` of that type, if `a` and `b` are both left-regular (meaning that multiplication on the left by either of these elements is an injective function), then the product of `a` and `b` is also left-regular. Simplified, if multiplying any element by `a` or `b` on the left always gives distinct results for distinct inputs, the same property holds true for the product of `a` and `b`.
More concisely: If `a` and `b` are left-regular elements in a semigroup `R`, then the product `a * b` is also left-regular in `R`.
|
AddUnits.isAddRegular
theorem AddUnits.isAddRegular : ∀ {R : Type u_1} [inst : AddMonoid R] (a : AddUnits R), IsAddRegular ↑a
The theorem `AddUnits.isAddRegular` states that for any type `R` that has an additive monoid structure, any element of `AddUnits R` (which represent the additive units of `R`) is add-regular. Being add-regular means that if the sum of `a` and any element `x` equals the sum of `a` and some other element `y`, then `x` must equal `y`. In other words, the operation of adding `a` is injective.
More concisely: For any type `R` with an additive monoid structure, every additive unit in `R` is injective with respect to addition.
|
IsAddRegular.all
theorem IsAddRegular.all : ∀ {R : Type u_1} [inst : Add R] [inst_1 : IsCancelAdd R] (g : R), IsAddRegular g
This theorem states that for any type `R` that has an addition operation and for which all additions are cancellative, every element `g` of type `R` is add-regular. In mathematical terms, this means that for every element `g` in `R`, if `g + a = g + b`, then `a = b`, and if `a + g = b + g`, then `a = b`, for all `a` and `b` in `R`.
More concisely: For any cancellative additive type `R`, every element `g` in `R` is such that `g + a = g + b` implies `a = b`, and `a + g = b + g` implies `a = b`.
|
isRegular_mul_and_mul_iff
theorem isRegular_mul_and_mul_iff :
∀ {R : Type u_1} [inst : Semigroup R] {a b : R},
IsRegular (a * b) ∧ IsRegular (b * a) ↔ IsRegular a ∧ IsRegular b
This theorem states that in any semigroup `R`, two elements `a` and `b` are regular if and only if both the product `a * b` and the product `b * a` are regular. This illustrates a connection between the regularity of individual elements `a` and `b` and the regularity of their products in either order.
More concisely: In a semigroup, elements `a` and `b` are regular if and only if their products `a * b` and `b * a` are regular.
|
isLeftRegular_zero_iff_subsingleton
theorem isLeftRegular_zero_iff_subsingleton :
∀ {R : Type u_1} [inst : MulZeroClass R], IsLeftRegular 0 ↔ Subsingleton R
This theorem states that the element `0` is left-regular if and only if the set `R` is trivial. In more detailed terms, for any type `R` that is a member of the `MulZeroClass` (in other words, a set with multiplication and zero elements such that multiplication by zero yields zero), the function of left-multiplication by `0` is injective (meaning that different inputs produce different outputs) if and only if `R` is a singleton or empty (a subsingleton). This means that the only way for `0` to be a left-regular element in a set is if that set contains at most one element.
More concisely: For any set `R` in `MulZeroClass`, the zero element `0` is left-regular if and only if `R` is a singleton or empty.
|
IsAddRightRegular.all
theorem IsAddRightRegular.all :
∀ {R : Type u_1} [inst : Add R] [inst_1 : IsRightCancelAdd R] (g : R), IsAddRightRegular g
The theorem states that for any type `R` equipped with an addition operation, if all additions can be cancelled from the right (i.e., for every `a`, `b`, and `c` in `R`, if `a + c = b + c` then `a = b`), then every element `g` in `R` is add-right-regular. In other words, adding `g` to any element on the right keeps the operation injective - no two different elements in `R` would map to the same result when `g` is added to them.
More concisely: If `R` is a type with additive infrastructure such that for all `a`, `b`, and `c` in `R`, `a + c = b + c` implies `a = b`, then every element `g` in `R` is right-cancelable with respect to addition.
|
IsAddLeftRegular.all
theorem IsAddLeftRegular.all :
∀ {R : Type u_1} [inst : Add R] [inst_1 : IsLeftCancelAdd R] (g : R), IsAddLeftRegular g
This theorem states that if in a type `R` equipped with an addition operation, left cancellation holds for all elements (i.e., for all `a`, `b`, and `c` in `R`, if `a + b = a + c` then `b = c`), then every element in `R` is add-left-regular. An element `g` being add-left-regular means that addition on the left by `g` is an injective function; in other words, for all `x` and `y` in `R`, if `g + x = g + y` then `x = y`.
More concisely: In a commutative ring `R` with left cancellation, every element is left-cancelable and additively left-invertible.
|
mul_isRightRegular_iff
theorem mul_isRightRegular_iff :
∀ {R : Type u_1} [inst : Semigroup R] {a : R} (b : R),
IsRightRegular a → (IsRightRegular (b * a) ↔ IsRightRegular b)
The theorem states that for all types `R` which have a `Semigroup` structure, and for all elements `a` of `R`, given an element `b` of `R`, if `a` is a right-regular element, then the right-regularity of the product `b * a` is equivalent to the right-regularity of `b`. In other words, an element is right-regular if and only if, when it is multiplied on the right by a right-regular element, the result is also right-regular. This is understood in the context of multiplication being a right-regular (i.e., right-cancellative) operation in the semigroup `R`.
More concisely: For all semigroups R and elements a, b in R, a is right-regular if and only if the product b * a is right-regular.
|
IsRegular.subsingleton
theorem IsRegular.subsingleton : ∀ {R : Type u_1} [inst : MulZeroClass R], IsRegular 0 → Subsingleton R
This theorem states that for any type `R` that has a multiplication and zero structure (`MulZeroClass`), the element `0` is regular if and only if `R` is a singleton type (i.e., a type with at most one element, `Subsingleton`). In other words, in a ring-like structure, if the zero element satisfies regularity conditions, then the structure is such that all its elements are identical.
More concisely: For any type `R` with a multiplication and zero structure, `0` is regular if and only if `R` is a singleton type.
|
isAddRegular_add_and_add_iff
theorem isAddRegular_add_and_add_iff :
∀ {R : Type u_1} [inst : AddSemigroup R] {a b : R},
IsAddRegular (a + b) ∧ IsAddRegular (b + a) ↔ IsAddRegular a ∧ IsAddRegular b
This theorem states that in any additive semigroup `R`, two elements `a` and `b` are add-regular if and only if the sums `a + b` and `b + a` are both add-regular. Here, being "add-regular" means that for any other elements `c` and `d` in the semigroup, if `a * c = a * d`, then `c = d`, and similarly for `b`. This property is symmetric with respect to the order of addition, as reflected in the use of both `a + b` and `b + a`.
More concisely: In an additive semigroup, two elements are add-regular if and only if the sums of those elements are also add-regular.
|
isRegular_one
theorem isRegular_one : ∀ {R : Type u_1} [inst : MulOneClass R], IsRegular 1
This theorem states that for any type `R` that has a multiplication and an identity element `1` (denoted by the `MulOneClass` typeclass), the identity element `1` is regular. In the context of ring theory, an element is regular if it is not a zero divisor. In other words, if for all non-zero elements `a` and `b` in `R`, if `1 * a = 1 * b`, then `a = b`, and if `a * 1 = b * 1`, then `a = b`.
More concisely: For any type `R` in Lean 4 belonging to the `MulOneClass` with identity element `1`, `1` is a regular element. In other words, for all non-zero `a, b` in `R`, `1 * a = 1 * b` implies `a = b` and `a * 1 = b * 1` implies `a = b`.
|
IsRegular.ne_zero
theorem IsRegular.ne_zero :
∀ {R : Type u_1} [inst : MulZeroClass R] {a : R} [inst_1 : Nontrivial R], IsRegular a → a ≠ 0
This theorem states that for any type `R` that is a multiplication-zero class and nontrivial, if an element `a` of `R` is regular, then `a` cannot be zero. In the context of algebra, a multiplication-zero class is a structure with multiplication and a zero element, where multiplication by zero yields zero. Nontrivial means that there are at least two distinct elements in the structure. A regular element is one for which multiplication is cancellable. Therefore, the theorem asserts that regular elements in such structures are always non-zero.
More concisely: In a multiplication-zero class `R` with at least two distinct elements, if an element `a` is regular, then `a` is non-zero.
|
IsRightRegular.mul
theorem IsRightRegular.mul :
∀ {R : Type u_1} [inst : Semigroup R] {a b : R}, IsRightRegular a → IsRightRegular b → IsRightRegular (a * b) := by
sorry
In the context of a semigroup, this theorem states that if two elements 'a' and 'b' are right-regular, then their product 'a * b' is also right-regular. Here, an element is right-regular if multiplying other elements from the semigroup by this element on the right results in distinct results for distinct elements, i.e., the multiplication operation on the right by this element is injective.
More concisely: If two right-regular elements in a semigroup have distinct elements on their right side, then their product is also right-regular.
|
Units.isRegular
theorem Units.isRegular : ∀ {R : Type u_1} [inst : Monoid R] (a : Rˣ), IsRegular ↑a
This theorem states that for any given monoid `R`, any element `a` in the group of units `Rˣ` of `R` is regular. In the context of ring theory, an element of a ring is called 'regular' if it is not a zero divisor, i.e., it does not multiply with a non-zero element to give zero. Therefore, this theorem guarantees that any element from the group of units in a monoid is not a zero divisor.
More concisely: In any monoid `R`, every unit `a` in `Rˣ` is a regular element.
|
isRegular_iff_subsingleton
theorem isRegular_iff_subsingleton : ∀ {R : Type u_1} [inst : MulZeroClass R], IsRegular 0 ↔ Subsingleton R
This theorem states that the element `0` is "regular" in a given multiplication-zero class `R` if and only if `R` is a "subsingleton". In the context of algebra, a "regular" element is one which satisfies certain properties with regards to operations in its set, and a "subsingleton" is a set with at most one element. Therefore, this theorem is making a claim about the structure of `R` based on the properties of `0` within it.
More concisely: The element 0 is regular in a multiplication-zero class R if and only if R is a set with at most one element.
|
not_isRightRegular_zero_iff
theorem not_isRightRegular_zero_iff : ∀ {R : Type u_1} [inst : MulZeroClass R], ¬IsRightRegular 0 ↔ Nontrivial R := by
sorry
The theorem states that in a multiplicative structure with a zero element (`MulZeroClass`), the zero element is not right-regular if and only if the structure is non-trivial. In other words, multiplication on the right by zero is not injective if and only if there is at least one pair of distinct elements in the structure. The notion of a structure being non-trivial in this context means that there exists at least one pair of elements in the structure that are not equal to each other.
More concisely: In a multiplicative structure with a zero element, the zero is not right-regular if and only if the structure contains distinct elements.
|
not_isLeftRegular_zero_iff
theorem not_isLeftRegular_zero_iff : ∀ {R : Type u_1} [inst : MulZeroClass R], ¬IsLeftRegular 0 ↔ Nontrivial R := by
sorry
This theorem states that in a non-trivial `MulZeroClass` (a mathematical structure that includes both multiplication and a zero element, and obeys certain rules), the `0` element is not left-regular. In other words, multiplication on the left by `0` is not injective. The theorem further establishes an equivalency between the non-injectivity of left-multiplication by `0` and the non-triviality of the `MulZeroClass`. Non-triviality in this context means that the zero element and the multiplication operation are distinct.
More concisely: In a non-trivial MulZeroClass, left multiplication by the zero element is not injective.
|
IsRegular.all
theorem IsRegular.all : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : IsCancelMul R] (g : R), IsRegular g
This theorem states that if for all elements in a type `R` that supports multiplication operation (`Mul R`), the multiplication operation is cancellative (`IsCancelMul R`), then every element `g` of `R` is regular (`IsRegular g`). Here, a regular element is one that is cancellative in both left and right multiplication, and cancellative means that the equation `a * b = a * c` implies `b = c`, and similarly for right multiplication.
More concisely: If `R` is a type with cancellative multiplication, then every element in `R` is regular.
|
isRightRegular_zero_iff_subsingleton
theorem isRightRegular_zero_iff_subsingleton :
∀ {R : Type u_1} [inst : MulZeroClass R], IsRightRegular 0 ↔ Subsingleton R
The theorem `isRightRegular_zero_iff_subsingleton` states that for any type `R` with a multiplication operation and a zero element (`MulZeroClass`), the zero element is considered right-regular (meaning that multiplying any element of `R` by zero on the right is an injective function) if and only if `R` is a subsingleton type. A subsingleton type is one that has at most one element, which in this context implies that `R` is a trivial ring, having only one element.
More concisely: The zero element of a type `R` with multiplication and a zero element is right-regular if and only if `R` is a trivial ring.
|
IsAddRegular.right
theorem IsAddRegular.right : ∀ {R : Type u_2} [inst : Add R] {c : R}, IsAddRegular c → IsAddRightRegular c
The theorem `IsAddRegular.right` states that for any type `R` that has an addition function, if an element `c` of type `R` is an add-regular element, then `c` is also a right-regular element. In other words, if addition by `c` is a regular operation (it is injective both when `c` is added to the left or to the right of any other element), then addition by `c` on the right is also injective. It bridges the concept of an add-regular element to an add-right-regular element in the context of a type with addition.
More concisely: If `R` is a type with an addition function and `c` is an add-regular element of `R`, then `c` is a right-regular element. In other words, if for all `x, y in R`, `x + c = y + c` implies `x = y`, then for all `x, y in R`, `x + c = y` implies `x = y`.
|
IsAddRightRegular.of_add
theorem IsAddRightRegular.of_add :
∀ {R : Type u_1} [inst : AddSemigroup R] {a b : R}, IsAddRightRegular (b + a) → IsAddRightRegular b
This theorem states that for any type `R` that is an additive semigroup, if an element `b` of `R` becomes "add-right-regular" after adding an "add-right-regular" element `a` to it on the right, then `b` itself is "add-right-regular". Here, an "add-right-regular" element `c` in `R` is defined as an element such that the function which adds `c` to any element on its right is injective, i.e., for any two different elements `x` and `y` in `R`, `x + c` differs from `y + c`.
More concisely: If `b` becomes add-right-regular after adding an add-right-regular element `a` to it in an additive semigroup `R`, then `b` is add-right-regular.
|
IsAddLeftRegular.of_add
theorem IsAddLeftRegular.of_add :
∀ {R : Type u_1} [inst : AddSemigroup R] {a b : R}, IsAddLeftRegular (a + b) → IsAddLeftRegular b
The theorem `IsAddLeftRegular.of_add` states that for any type `R` with an addition operation (forming an additive semigroup), if an element `b` of `R` becomes add-left-regular when an add-left-regular element `a` is added to it from the left, then `b` itself is also an add-left-regular element. Here, an element is considered add-left-regular if the function that adds it to any other element from the left is injective, meaning each input maps to a unique output.
More concisely: If an element `b` in an additive semigroup `R` becomes add-left-regular when an add-left-regular element `a` is added to it from the left, then `b` is also an add-left-regular element.
|
not_isRegular_zero
theorem not_isRegular_zero : ∀ {R : Type u_1} [inst : MulZeroClass R] [inst_1 : Nontrivial R], ¬IsRegular 0
This theorem states that in a non-trivial ring, the zero element is not regular. Here, a ring is 'non-trivial' if it contains at least two distinct elements. The 'regular' property of an element in a ring refers to the condition that multiplication by that element, from left or right, is injective. Hence, this theorem basically asserts that multiplication by zero cannot be injective in any non-trivial ring, which means there are no elements that when multiplied by zero give a non-zero result.
More concisely: In a non-trivial ring, the zero element is not regular (i.e., multiplication by zero is not injective).
|