add_neg_cancel_comm
theorem add_neg_cancel_comm : ∀ {G : Type u_1} [inst : AddCommGroup G] (a b : G), a + b + -a = b
This theorem states that for any given type `G` which forms an additive commutative group, for any elements `a` and `b` of this group, adding `a` to `b`, then adding the additive inverse of `a`, results in `b`. This essentially shows that adding an element and its negation (in any order, due to commutativity) will cancel out, leaving us with the other element. This is a property related to the additive identity in an additive commutative group.
More concisely: For any additive commutative group `G` and elements `a, b` in `G`, `a + (-a) = b` if and only if `a = b`.
|
succ_nsmul'
theorem succ_nsmul' : ∀ {M : Type u_2} [inst : AddMonoid M] (a : M) (n : ℕ), (n + 1) • a = a + n • a
This theorem states that for any type `M` that is an instance of an Additive Monoid, and for any element `a` of this type `M` and natural number `n`, the scalar multiplication of `n + 1` with `a` is equal to `a` added to the scalar multiplication of `n` with `a`. This is essentially a property of distributivity in additive monoids.
More concisely: For any additive monoid M and its element a, and natural number n, the operation of scaling by n+1 is equal to the operation of scaling by n followed by adding a to the result. (a.k.a. Distributivity of scaling over addition in additive monoids)
|
AddCommute.nsmul_left
theorem AddCommute.nsmul_left :
∀ {M : Type u_2} [inst : AddMonoid M] {a b : M}, AddCommute a b → ∀ (n : ℕ), AddCommute (n • a) b
This theorem states that for any type `M` that is an additive monoid, and any two elements `a` and `b` of `M` that commute under addition, together with any natural number `n`, the `n`-fold addition of `a` (denoted `n • a`) still commutes with `b`. In other words, if `a + b = b + a`, then `n * a + b = b + n * a` for all natural numbers `n`, where `*` denotes the repeated addition.
More concisely: For any additive monoid `M` and commuting elements `a, b` in `M`, the `n`-fold addition of `a` commutes with `b` for all natural numbers `n`, i.e., `n • a + b = b + n • a`.
|
add_neg_cancel_comm_assoc
theorem add_neg_cancel_comm_assoc : ∀ {G : Type u_1} [inst : AddCommGroup G] (a b : G), a + (b + -a) = b
This theorem, `add_neg_cancel_comm_assoc`, states that for all types `G` that form an additive commutative group, for any two elements `a` and `b` belonging to this group `G`, the sum of `a` and the sum of `b` and the additive inverse of `a` is equal to `b`. In other words, adding `a` to `b` and then subtracting `a` returns `b`, which is essentially the property of cancellation in the group.
More concisely: For all additive commutative groups G and elements a, b in G, a + b + (-a) = b.
|
AddCommute.nsmul_nsmul
theorem AddCommute.nsmul_nsmul :
∀ {M : Type u_2} [inst : AddMonoid M] {a b : M}, AddCommute a b → ∀ (m n : ℕ), AddCommute (m • a) (n • b) := by
sorry
This theorem states that for any given type `M` which is an additive monoid, if two elements `a` and `b` of `M` commute additively (i.e., `a + b = b + a`), then for any two natural numbers `m` and `n`, the `m`-fold repeated addition of `a` (denoted `m • a`) and the `n`-fold repeated addition of `b` (denoted `n • b`) also commute additively. In other words, if `a` and `b` commute, then `m • a + n • b = n • b + m • a` holds true for all natural numbers `m` and `n`. Here, `•` denotes the nsmul operation in Lean, which is equivalent to repeated addition.
More concisely: If `a` and `b` are commuting elements of an additive monoid `M`, then for all natural numbers `m` and `n`, `m • a + n • b = n • b + m • a`.
|
AddCommute.add_add_add_comm
theorem AddCommute.add_add_add_comm :
∀ {S : Type u_2} [inst : AddSemigroup S] {b c : S},
AddCommute b c → ∀ (a d : S), a + b + (c + d) = a + c + (b + d)
This theorem, `AddCommute.add_add_add_comm`, states that for any type `S` that has an addition operation (forming an additive semigroup), if two elements `b` and `c` commute under addition (i.e., `b + c = c + b`), then for all elements `a` and `d` in `S`, the equation `a + b + (c + d) = a + c + (b + d)` will hold. In other words, if `b` and `c` can be added in either order without changing the result, then you can rearrange the addition of four elements `a`, `b`, `c`, `d` in a specific way without changing the sum.
More concisely: For any additive semigroup `S` and elements `a`, `b`, `c`, `d` in `S` with `b` and `c` commuting under addition, `a + b + (c + d) = a + c + (b + d)`.
|
Commute.mul_mul_mul_comm
theorem Commute.mul_mul_mul_comm :
∀ {S : Type u_2} [inst : Semigroup S] {b c : S}, Commute b c → ∀ (a d : S), a * b * (c * d) = a * c * (b * d) := by
sorry
The theorem `Commute.mul_mul_mul_comm` states that for any semigroup `S` and any two elements `b` and `c` in `S` that commute, for any additional elements `a` and `d` in `S`, the result of multiplying `a`, `b`, `c`, and `d` together in the order `a * b * (c * d)` is equal to the result of multiplying them in the order `a * c * (b * d)`. In other words, it establishes a specific form of associativity and commutativity in the multiplication of four elements when two of them commute.
More concisely: For any semigroup `S` and commuting elements `b` and `c` in `S`, the order of multiplication of elements `a`, `b`, `c`, and `d` does not affect the result: `(a * b * (c * d)) = (a * c * (b * d))`.
|
Commute.one_right
theorem Commute.one_right : ∀ {M : Type u_2} [inst : MulOneClass M] (a : M), Commute a 1
The theorem `Commute.one_right` states that for any type `M` equipped with multiplication and identity element (`MulOneClass`) and any element `a` of type `M`, the element `a` commutes with the identity element `1`. In other words, the multiplication of `a` with 1 is the same as the multiplication of 1 with `a` - their order in the multiplication does not matter, or in mathematical terms, `a * 1 = 1 * a`.
More concisely: For any `MulOneClass` type `M` and element `a` in `M`, `a * 1 = 1 * a`.
|
AddCommute.nsmul_right
theorem AddCommute.nsmul_right :
∀ {M : Type u_2} [inst : AddMonoid M] {a b : M}, AddCommute a b → ∀ (n : ℕ), AddCommute a (n • b)
This theorem states that if addition of two elements `a` and `b` of a type `M` (that forms an additive monoid) is commutative, i.e., `a + b = b + a`, then addition of `a` and any natural number multiple of `b` is also commutative. In other words, if `a` and `b` commute additively, then `a` and `n•b` will also commute additively for any natural number `n`. Here, `n•b` represents the operation of adding `b` to itself `n` times.
More concisely: If `a` and `b` commute in an additive monoid `M` (i.e., `a + b = b + a`), then for any natural number `n`, `a` and `n` times `b` (`n•b`) also commute in `M` (i.e., `a + n•b = n•b + a`).
|
Commute.right_comm
theorem Commute.right_comm :
∀ {S : Type u_2} [inst : Semigroup S] {b c : S}, Commute b c → ∀ (a : S), a * b * c = a * c * b
This theorem, named `Commute.right_comm`, states that for any type `S` that forms a semigroup, if two elements `b` and `c` commute (i.e., `b * c = c * b`), then for any element `a` from the same semigroup, the multiplication `a * b * c` is equal to `a * c * b`. Essentially, this theorem is asserting the right multiplication commutivity when `b` and `c` commute.
More concisely: For any semigroup `S` and elements `a`, `b`, and `c` in `S` such that `b * c = c * b`, it follows that `a * b * c = a * c * b`.
|
pow_succ'
theorem pow_succ' : ∀ {M : Type u_2} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a * a ^ n
This theorem states that for any type `M` that is a monoid, and for any element `a` of that type and any natural number `n`, raising `a` to the power of `n+1` is equivalent to multiplying `a` by itself raised to the power of `n`. This is a property of exponentiation in a monoid structure.
More concisely: For any monoid `M` and its element `a`, the exponentiation `a ^ (n + 1)` is equivalent to the repeated multiplication `a ^ n * a`.
|
Commute.pow_right
theorem Commute.pow_right : ∀ {M : Type u_2} [inst : Monoid M] {a b : M}, Commute a b → ∀ (n : ℕ), Commute a (b ^ n)
This theorem states that for any type `M` that forms a monoid, if two elements `a` and `b` of `M` commute, then `a` also commutes with any natural number power of `b`. In mathematical terms, if `a * b = b * a` (i.e., `a` and `b` commute), then for any natural number `n`, `a * b^n = b^n * a`.
More concisely: If `a` and `b` are commuting elements of a monoid `M`, then `a` commutes with any natural power of `b`, i.e., `a * b^n = b^n * a` for all natural numbers `n`.
|
Commute.one_left
theorem Commute.one_left : ∀ {M : Type u_2} [inst : MulOneClass M] (a : M), Commute 1 a
This theorem, `Commute.one_left`, states that for any type `M` that has a multiplication and one identity operation (captured by `MulOneClass M`), the number 1 commutes with any element `a` of type `M`. In other words, in the context of multiplication, multiplying 1 with any element `a` (`1 * a`) is the same as multiplying `a` with 1 (`a * 1`).
More concisely: For any type `M` with multiplication and identity operation, 1 and any element `a` in `M` commute in multiplication: `1 * a = a * 1`.
|
AddCommute.all
theorem AddCommute.all : ∀ {S : Type u_2} [inst : AddCommMagma S] (a b : S), AddCommute a b
This theorem states that for any type `S` which is an additive commutative magma (that is, the operation of addition `+` is defined and is commutative on `S`), and for any two elements `a` and `b` of `S`, the property `AddCommute a b` holds. In other words, for any two elements `a` and `b` in a commutative magma, their addition is commutative: `a + b = b + a`.
More concisely: In any commutative magma `S`, for all `a, b` in `S`, `a + b = b + a`.
|
Commute.pow_left
theorem Commute.pow_left : ∀ {M : Type u_2} [inst : Monoid M] {a b : M}, Commute a b → ∀ (n : ℕ), Commute (a ^ n) b
The theorem `Commute.pow_left` states that for any type `M` with a defined Monoid structure, if two elements `a` and `b` commute (i.e., `a * b = b * a`), then `a` raised to any natural number `n` commutes with `b`. In other words, if `a` and `b` commute, then `a^n * b = b * a^n` for any natural number `n`.
More concisely: If `a` and `b` are commuting elements of a monoid `M`, then `a^n * b = b * a^n` for all natural numbers `n`.
|
AddCommute.add_right
theorem AddCommute.add_right :
∀ {S : Type u_2} [inst : AddSemigroup S] {a b c : S}, AddCommute a b → AddCommute a c → AddCommute a (b + c) := by
sorry
The theorem states that for any type `S` that forms an additive semigroup, if an element `a` of `S` commutes additively with two elements `b` and `c` (i.e., `a + b = b + a` and `a + c = c + a`), then `a` also commutes additively with the sum of `b` and `c` (i.e., `a + (b + c) = (b + c) + a`).
More concisely: If `a` commutes additively with `b` and `c` in an additive semigroup `S`, then `a` commutes additively with their sum `b + c`.
|
Commute.symm
theorem Commute.symm : ∀ {S : Type u_2} [inst : Mul S] {a b : S}, Commute a b → Commute b a
The theorem `Commute.symm` states that for any type `S` that has a multiplication operation, if two elements `a` and `b` of `S` commute with each other (that is, `a * b = b * a`), then `b` and `a` also commute with each other (i.e., `b * a = a * b`). This theorem expresses the symmetry of the commutation relation in a multiplicative structure.
More concisely: If `a` and `b` in a multiplicative type `S` commute (i.e., `a * b = b * a`), then they symmetically commute (`b * a = a * b`).
|
Commute.eq
theorem Commute.eq : ∀ {S : Type u_2} [inst : Mul S] {a b : S}, Commute a b → a * b = b * a
The theorem `Commute.eq` states that for any type `S` equipped with a multiplication operation, if two elements `a` and `b` of `S` commute (that is, `a * b = b * a`), then the product of `a` and `b` is equal to the product of `b` and `a`. In other words, this theorem provides a way of rewriting commutative multiplications in a different order.
More concisely: If `a` and `b` are commuting elements of a multiplicative monoid `S`, then `a * b = b * a`. Hence, `a * b` is equal to `b * a`.
|
AddCommute.refl
theorem AddCommute.refl : ∀ {S : Type u_2} [inst : Add S] (a : S), AddCommute a a
This theorem states that for any type `S` that has an addition operation, any element `a` of type `S` commutes with itself. In the context of addition, "commuting" means that the order of the operands does not affect the result, hence `a + a = a + a`. This is a universal property, applicable to all elements of any type that allows addition.
More concisely: For any type `S` with an addition operation, the commutative law holds: `a + a = a + a` for all `a` in `S`.
|
Commute.all
theorem Commute.all : ∀ {S : Type u_2} [inst : CommMagma S] (a b : S), Commute a b
This theorem states that for any type `S` that forms a commutative magma (i.e., a set equipped with an associative and commutative binary operation), and for any two elements `a` and `b` of `S`, `a` and `b` commute. In other words, multiplying `a` and `b` in either order gives the same result, formally expressed as `a * b = b * a`.
More concisely: For any commutative magma `S` and elements `a`, `b` in `S`, `a * b` equals `b * a`.
|
Commute.symm_iff
theorem Commute.symm_iff : ∀ {S : Type u_2} [inst : Mul S] {a b : S}, Commute a b ↔ Commute b a
This theorem states that for any type `S` equipped with a multiplication operation (`Mul`), and for any two elements `a` and `b` of this type, `a` and `b` commute (i.e., `a * b = b * a`) if and only if `b` and `a` commute. In other words, the commutativity of two elements is symmetric: if `a` commutes with `b`, then `b` commutes with `a`, and vice versa.
More concisely: For any type `S` with multiplication `Mul`, and for all `a` and `b` in `S`, `a` commutes with `b` if and only if `b` commutes with `a`.
|
mul_inv_cancel_comm
theorem mul_inv_cancel_comm : ∀ {G : Type u_1} [inst : CommGroup G] (a b : G), a * b * a⁻¹ = b
This theorem, `mul_inv_cancel_comm`, states that for any commutative group `G` and any two elements `a` and `b` of `G`, if you multiply `a` and `b` and then multiply the result by the inverse of `a`, you get back `b`. This effectively states that multiplication by `a` and its inverse `a⁻¹` cancels out, regardless of their position. The order of multiplication doesn't matter due to the commutative property of the group.
More concisely: For all commutative groups G and elements a, b in G, a * b * a⁻¹ = b.
|
Commute.mul_left
theorem Commute.mul_left :
∀ {S : Type u_2} [inst : Semigroup S] {a b c : S}, Commute a c → Commute b c → Commute (a * b) c
The theorem `Commute.mul_left` states that in the context of a semigroup, if two elements (`a` and `b`) each commute with a third element (`c`), meaning that the order of multiplication does not change the result (`a * c = c * a` and `b * c = c * b`), then the product of the two elements (`a * b`) also commutes with the third element (`c`). In other words, `(a * b) * c = c * (a * b)`. This theorem holds for any type `S` that is an instance of a semigroup.
More concisely: In a semigroup, if elements `a`, `b`, and `c` mutually commute (i.e., `a * c = c * a` and `b * c = c * b`), then their product `a * b` also commutes with `c` (i.e., `(a * b) * c = c * (a * b)`).
|
AddCommute.add_left
theorem AddCommute.add_left :
∀ {S : Type u_2} [inst : AddSemigroup S] {a b c : S}, AddCommute a c → AddCommute b c → AddCommute (a + b) c := by
sorry
This theorem states that in the context of an additive semigroup `S`, if two elements `a` and `b` both commute with another element `c` (that is, `a + c = c + a` and `b + c = c + b`), then the sum of `a` and `b` also commutes with `c`, (i.e., `(a + b) + c = c + (a + b)`).
More concisely: In an additive semigroup, if elements `a` and `b` commute with a common element `c`, then `a + b` and `c` commute. (i.e., `(a + b) + c = c + (a + b)`)
|
Commute.mul_right
theorem Commute.mul_right :
∀ {S : Type u_2} [inst : Semigroup S] {a b c : S}, Commute a b → Commute a c → Commute a (b * c)
The theorem `Commute.mul_right` states that: for any type `S` that forms a semigroup, if an element `a` of `S` commutes with two other elements `b` and `c` of `S` (i.e., `a * b = b * a` and `a * c = c * a`), then `a` also commutes with the product of `b` and `c` (i.e., `a * (b * c) = (b * c) * a`).
More concisely: If `a` commutes with both `b` and `c` in a semigroup `S`, then `a` commutes with their product `b * c`.
|
AddCommute.right_comm
theorem AddCommute.right_comm :
∀ {S : Type u_2} [inst : AddSemigroup S] {b c : S}, AddCommute b c → ∀ (a : S), a + b + c = a + c + b
The theorem `AddCommute.right_comm` states that for any type `S` that is an additive semigroup, if two elements `b` and `c` of `S` commute under addition (i.e., `b + c = c + b`), then for any other element `a` of `S`, the sum `a + b + c` is equal to the sum `a + c + b`. In other words, if `b` and `c` commute, then adding `b` and `c` to `a` in any order results in the same sum.
More concisely: For any additive semigroup `S` and commuting elements `b` and `c` in `S`, `b + c = c + b` implies `a + b + c = a + c + b` for all `a` in `S`.
|
Commute.left_comm
theorem Commute.left_comm :
∀ {S : Type u_2} [inst : Semigroup S] {a b : S}, Commute a b → ∀ (c : S), a * (b * c) = b * (a * c)
The theorem `Commute.left_comm` states that for any type `S` that forms a semigroup, and for any elements `a` and `b` in `S` that commute, for any element `c` in `S`, the operation `a * (b * c)` is equal to `b * (a * c)`. In other words, if `a` and `b` commute, then `a` and `b` can be interchanged in multiplication without affecting the result, even when they are multiplied with another element `c`. This property is known as the left commutativity in mathematics.
More concisely: For any semigroup `S` and commuting elements `a` and `b` in `S`, `a * (b * c)` equals `b * (a * c)` for all `c` in `S`.
|
Commute.self_pow
theorem Commute.self_pow : ∀ {M : Type u_2} [inst : Monoid M] (a : M) (n : ℕ), Commute a (a ^ n)
This theorem states that for any monoid `M` and any element `a` in `M`, `a` commutes with its own power `a^n`, for any natural number `n`. In other words, in the context of a given monoid, the multiplication of any element with its own power is commutative, i.e., `a * a^n = a^n * a`.
More concisely: For any monoid `M` and its element `a`, the power `a^n` commutes with `a`, i.e., `a * a^n = a^n * a` for all natural numbers `n`.
|
Commute.refl
theorem Commute.refl : ∀ {S : Type u_2} [inst : Mul S] (a : S), Commute a a
This theorem states that for any type `S` that has a multiplication operation, any element `a` in `S` commutes with itself. In other words, for any `a` in `S`, the multiplication of `a` with itself results in the same output as the multiplication of itself with `a`. In mathematical terms, it is expressing that `a * a = a * a` for all `a` in `S`.
More concisely: For all types `S` with a multiplication operation and for all elements `a` in `S`, `a * a` equals `a * a`. In mathematical notation, `∀ (S : Type) [Mul S], ∀ (a : S), a * a = a * a`.
|
AddCommute.eq
theorem AddCommute.eq : ∀ {S : Type u_2} [inst : Add S] {a b : S}, AddCommute a b → a + b = b + a
This theorem states that for any type `S` equipped with an addition operation, and for any two elements `a` and `b` of type `S`, if `a` and `b` commute with respect to addition (i.e., `a + b` equals `b + a`), then the result of adding `a` and `b` is indeed equal to the result of adding `b` and `a`. This theorem can be practical for rewriting expressions involving the addition operation in Lean 4 proof scripts.
More concisely: For any commutative additive type `S` and elements `a, b` in `S`, `a + b` equals `b + a`.
|
AddCommute.symm
theorem AddCommute.symm : ∀ {S : Type u_2} [inst : Add S] {a b : S}, AddCommute a b → AddCommute b a
The theorem `AddCommute.symm` states that for any type `S` that has an addition operation, if two elements `a` and `b` of type `S` satisfy the property `AddCommute a b` (meaning that `a + b = b + a`), then they also satisfy `AddCommute b a` (meaning that `b + a = a + b`). In other words, the commutativity of addition is symmetric: if `a` commutes with `b`, then `b` commutes with `a`.
More concisely: If `a` and `b` are elements of a type `S` with commutative addition, then `AddCommute a b` implies `AddCommute b a`.
|
Commute.pow_pow
theorem Commute.pow_pow :
∀ {M : Type u_2} [inst : Monoid M] {a b : M}, Commute a b → ∀ (m n : ℕ), Commute (a ^ m) (b ^ n)
The theorem `Commute.pow_pow` states that for any type `M` that forms a monoid, and for any elements `a` and `b` of type `M` that commute, meaning `a * b = b * a`, then for any non-negative integers `m` and `n`, the `m`-th power of `a` and the `n`-th power of `b` also commute. In other words, if `a` and `b` commute, then `(a ^ m) * (b ^ n) = (b ^ n) * (a ^ m)` for all non-negative integers `m` and `n`.
More concisely: For any monoid `M` and commuting elements `a, b` in `M`, the powers `a^m` and `b^n` commute for all non-negative integers `m` and `n`, that is, `a^m * b^n = b^n * a^m`.
|