Commute.neg_right
theorem Commute.neg_right :
∀ {R : Type x} [inst : Mul R] [inst_1 : HasDistribNeg R] {a b : R}, Commute a b → Commute a (-b)
This theorem, `Commute.neg_right`, states that for any type `R` that has multiplication (`Mul`) and a distributive negation relation (`HasDistribNeg`), if two elements `a` and `b` of `R` commute, i.e., `a * b = b * a`, then `a` also commutes with the negation of `b`, i.e., `a * (-b) = (-b) * a`.
More concisely: If `R` is a type with multiplication and distributive negation, and `a` and `b` in `R` commute, then `a` also commutes with the negation of `b`. In other words, `a * b = b * a` implies `a * (-b) = (-b) * a`.
|
mul_self_eq_mul_self_iff
theorem mul_self_eq_mul_self_iff :
∀ {R : Type x} [inst : CommRing R] [inst_1 : NoZeroDivisors R] {a b : R}, a * a = b * b ↔ a = b ∨ a = -b
This theorem states that for any type `R` which is a commutative ring with no zero divisors, and for any two elements `a` and `b` from `R`, the statement "the square of `a` is equal to the square of `b`" is equivalent to the statement "`a` is equal to `b` or `a` is equal to negative `b`". In mathematical notation, this is saying that if \(a^2 = b^2\), then either \(a = b\) or \(a = -b\).
More concisely: For any commutative ring with no zero divisors R and elements a, b ∈ R, a² = b² if and only if a = b or a = -b.
|
mul_self_eq_one_iff
theorem mul_self_eq_one_iff :
∀ {R : Type x} [inst : NonAssocRing R] [inst_1 : NoZeroDivisors R] {a : R}, a * a = 1 ↔ a = 1 ∨ a = -1
This theorem states that for any type `R` that forms a non-associative ring without zero divisors, for any element `a` of that type, the condition of `a` multiplied by itself being equal to 1 is equivalent to `a` being either 1 or -1. This means that in such a ring, the only solutions to the equation `a * a = 1` are `a = 1` and `a = -1`.
More concisely: In a non-associative ring without zero divisors `R`, an element `a` satisfies `a * a = 1` if and only if `a` is equal to `1` or `-1`.
|
Units.inv_eq_self_iff
theorem Units.inv_eq_self_iff :
∀ {R : Type x} [inst : Ring R] [inst_1 : NoZeroDivisors R] (u : Rˣ), u⁻¹ = u ↔ u = 1 ∨ u = -1
This theorem states that in the unit group of an integral domain, a unit 'u' is its own multiplicative inverse if and only if 'u' is either 1 or -1. An integral domain here is a specific type of ring 'R' that doesn't allow for zero divisors. The symbol 'Rˣ' represents the group of units in the ring 'R', and 'u⁻¹' is the multiplicative inverse of the unit 'u'.
More concisely: In an integral domain, a unit has a multiplicative inverse if and only if it is 1 or -1.
|
Commute.mul_self_sub_mul_self_eq
theorem Commute.mul_self_sub_mul_self_eq :
∀ {R : Type x} [inst : NonUnitalNonAssocRing R] {a b : R}, Commute a b → a * a - b * b = (a + b) * (a - b) := by
sorry
The theorem `Commute.mul_self_sub_mul_self_eq` states that for any type `R` that forms a `NonUnitalNonAssocRing`, given two elements `a` and `b` of type `R` that commute (meaning `a * b = b * a`), the difference of their squares (`a * a - b * b`) is equal to the product of `a + b` and `a - b`. This is a well-known algebraic identity often referred to as the difference of squares formula.
More concisely: For any commuting elements `a` and `b` in a non-unital non-associative ring `R`, their squared difference `(a * a) - (b * b)` equals the product of their sum and difference `(a + b) * (a - b)`.
|
Commute.add_left
theorem Commute.add_left :
∀ {R : Type x} [inst : Distrib R] {a b c : R}, Commute a c → Commute b c → Commute (a + b) c
This theorem states that for any type `R` that has a distributive operation, if two elements `a` and `c` commute (i.e., `a * c = c * a`) and two elements `b` and `c` also commute, then the sum of `a` and `b` commutes with `c` (i.e., `(a + b) * c = c * (a + b)`). In other words, if multiplication by `c` commutes with both `a` and `b`, then it also commutes with the sum of `a` and `b`. This theorem is a statement about the commutativity of multiplication over addition in distributive structures.
More concisely: If `R` is a distributive type with commutative multiplication, and `a`, `b`, and `c` are commuting elements, then `(a + b) * c = c * (a + b)`.
|
Commute.sub_left
theorem Commute.sub_left :
∀ {R : Type x} [inst : NonUnitalNonAssocRing R] {a b c : R}, Commute a c → Commute b c → Commute (a - b) c := by
sorry
The theorem `Commute.sub_left` states that for any type `R` that forms a non-unital, non-associative ring, and for any three elements `a`, `b`, and `c` of this type, if `a` commutes with `c` and `b` commutes with `c`, then the difference of `a` and `b` also commutes with `c`. Here, two elements are said to commute if their multiplication is commutative, that is, `a * c = c * a` and `b * c = c * b` implies `(a - b) * c = c * (a - b)`.
More concisely: If `R` is a non-unital, non-associative ring and `a`, `b`, and `c` are elements of `R` such that `a` commutes with `c` and `b` commutes with `c`, then `(a - b)` commutes with `c`, i.e., `c * (a - b) = (a - b) * c`.
|
mul_self_sub_mul_self
theorem mul_self_sub_mul_self : ∀ {R : Type x} [inst : CommRing R] (a b : R), a * a - b * b = (a + b) * (a - b) := by
sorry
This theorem states that in any commutative ring `R`, for any two elements `a` and `b` of `R`, the difference of their squares (`a * a - b * b`) can be expressed as the product of the sum and difference of `a` and `b` (`(a + b) * (a - b)`). This is a formalization of the well-known algebraic identity $(a^2 - b^2) = (a + b)(a - b)$.
More concisely: In any commutative ring, the difference of two elements' squares equals the product of their sum and difference.
|
Commute.add_right
theorem Commute.add_right :
∀ {R : Type x} [inst : Distrib R] {a b c : R}, Commute a b → Commute a c → Commute a (b + c)
This theorem states that for any type `R` that has a distributive property (denoted by `[inst : Distrib R]`), if two elements `a` and `b` commute, and `a` and `c` also commute, then `a` commutes with the sum of `b` and `c`. In other words, if `a * b = b * a` and `a * c = c * a`, then `a * (b + c) = (b + c) * a`. This is a property that is closely related to the distributivity of multiplication over addition in the given type `R`.
More concisely: If `R` is a distributive type with elements `a`, `b`, and `c` such that `a` commutes with both `b` and `c`, then `a` commutes with their sum, `b + c`. That is, `a * (b + c) = (b + c) * a`.
|