IsAddCentral.mid_assoc
theorem IsAddCentral.mid_assoc :
∀ {M : Type u_1} [inst : Add M] {z : M}, IsAddCentral z → ∀ (a c : M), a + z + c = a + (z + c)
This theorem, named `IsAddCentral.mid_assoc`, describes the middle associative property of addition in a general algebraic structure. Specifically, it states that for any type `M` equipped with an addition operation, any element `z` of `M` that satisfies the property `IsAddCentral`, and any elements `a` and `c` of `M`, the equality `a + z + c = a + (z + c)` holds. In other words, when adding `z` in the middle of `a` and `c`, it doesn't matter whether we group `z` and `c` together first or not; the result will be the same.
More concisely: For any type `M` with an addition operation and any `IsAddCentral` element `z` in `M`, the addition is middle associative: `a + z + c = a + (z + c)` for all `a, c` in `M`.
|
IsMulCentral.mid_assoc
theorem IsMulCentral.mid_assoc :
∀ {M : Type u_1} [inst : Mul M] {z : M}, IsMulCentral z → ∀ (a c : M), a * z * c = a * (z * c)
This theorem, named 'IsMulCentral.mid_assoc', states that for any type 'M' equipped with multiplication, and for any element 'z' of type 'M' that is a multiplication central element, the 'middle associative multiplication property' holds. In other words, for any two elements 'a' and 'c' of type 'M', the product of 'a', 'z', and 'c', regardless of whether 'z' is multiplied with 'a' first or with 'c', is the same. Mathematically, this can be written as $a * z * c = a * (z * c)$.
More concisely: For any type equipped with multiplication and any multiplication central element z, the middle associativity property holds: i.e., a * z * c = a * (z * c) for all elements a and c.
|
IsMulCentral.left_comm
theorem IsMulCentral.left_comm :
∀ {M : Type u_1} {a : M} [inst : Mul M], IsMulCentral a → ∀ (b c : M), a * (b * c) = b * (a * c)
The theorem `IsMulCentral.left_comm` states that for any type `M` with a multiplication operation (denoted by `Mul M`), and for any element `a` of type `M` that is central with respect to multiplication (i.e., satisfies `IsMulCentral a`), the left multiplication of `a` commutes with the multiplication of any two other elements `b` and `c` of type `M`. That is, the expression `a * (b * c)` is equal to the expression `b * (a * c)`. This essentially means that `a` can be moved around in multiplication expressions without changing the result.
More concisely: For any type `M` with multiplication and any central element `a` in `M`, we have `a * (b * c) = b * (a * c)` for all `b, c` in `M`.
|
Set.center_units_eq
theorem Set.center_units_eq : ∀ {M : Type u_1} [inst : GroupWithZero M], Set.center Mˣ = Units.val ⁻¹' Set.center M
This theorem states that, for any type `M` that has a `GroupWithZero` structure, the center of the group of units of `M` is equal to the preimage of the center of `M` under the function that returns the underlying value of a unit. In other words, an element is in the center of the group of units if and only if its underlying value is in the center of the original group with zero. The "center" of a group consists of elements that commute with all other elements, i.e., for any element `z` in the center and any element `m` in the group, `z * m = m * z`.
More concisely: The center of the group of units of a `GroupWithZero` type `M` equals the preimage of the center of `M` under the underlying value function.
|
Set.mul_mem_center
theorem Set.mul_mem_center :
∀ {M : Type u_1} [inst : Mul M] {z₁ z₂ : M}, z₁ ∈ Set.center M → z₂ ∈ Set.center M → z₁ * z₂ ∈ Set.center M := by
sorry
The theorem `Set.mul_mem_center` states that for any type `M` equipped with a multiplication operation (`Mul M`), if two elements `z₁` and `z₂` belong to the center of the magma `M` (i.e., they commute with every other element in `M`), then their product `z₁ * z₂` also belongs to the center of `M`. In other words, the center of a magma is closed under the magma's multiplication operation.
More concisely: The center of a magma is a submonoid that is closed under multiplication.
|
IsAddCentral.comm
theorem IsAddCentral.comm : ∀ {M : Type u_1} [inst : Add M] {z : M}, IsAddCentral z → ∀ (a : M), z + a = a + z := by
sorry
This theorem states that for any type `M` that has an addition operation and any element `z` of type `M` that satisfies the property `IsAddCentral`, addition of `z` and any other element `a` of `M` is commutative. In other words, adding `z` to `a` is the same as adding `a` to `z`. This could be written in LaTeX as: for all `a` in `M`, `z + a = a + z`.
More concisely: For any type `M` with additions and any `IsAddCentral` element `z` in `M`, the addition is commutative, i.e., `z + a = a + z` for all `a` in `M`.
|
IsMulCentral.comm
theorem IsMulCentral.comm : ∀ {M : Type u_1} [inst : Mul M] {z : M}, IsMulCentral z → ∀ (a : M), z * a = a * z := by
sorry
This theorem states that multiplication is commutative under certain conditions. Specifically, for any type `M` that has a multiplication operation and any element `z` of type `M`, if `z` satisfies the condition `IsMulCentral`, then for any other element `a` of type `M`, the product of `z` and `a` is the same whether `z` is multiplied with `a` or `a` is multiplied with `z`. In other words, if `z` belongs to the center of a multiplication operation, it commutes with every other element under that operation.
More concisely: If `M` is a type with multiplication and `z` is an element of `M` satisfying `IsMulCentral`, then for all `a` in `M`, `z * a = a * z`.
|
Set.mem_center_iff
theorem Set.mem_center_iff : ∀ (M : Type u_1) [inst : Mul M] {z : M}, z ∈ Set.center M ↔ IsMulCentral z
This theorem states that for any type `M` with a multiplication operation (represented by `[inst : Mul M]`), an element `z` of type `M` belongs to the center of `M` (i.e., `z` is in `Set.center M`) if and only if `z` is a "multiplication central" element (represented by `IsMulCentral z`).
In mathematical terms, this might be understood as telling us that an element is in the center of a multiplicative set (e.g., a group or ring in abstract algebra) if and only if it commutes with all other elements in the set under multiplication. The "if and only if" (represented by `↔` in Lean 4) denotes that both conditions imply each other.
More concisely: An element `z` of a type `M` with multiplication belongs to the center if and only if it is multiplication central, i.e., commutes with all elements under multiplication.
|
IsMulCentral.left_assoc
theorem IsMulCentral.left_assoc :
∀ {M : Type u_1} [inst : Mul M] {z : M}, IsMulCentral z → ∀ (b c : M), z * (b * c) = z * b * c
The theorem `IsMulCentral.left_assoc` establishes the associative property for left multiplication in a given type `M` that possesses a multiplication operation. The theorem asserts that for all elements `z`, `b`, and `c` from `M`, where `z` is a central element (meaning for all `x` in `M`, `z * x = x * z`), the equation `z * (b * c) = z * b * c` always holds true. This essentially means that the order in which the multiplication operations are performed does not impact the result.
More concisely: For all central elements `z` in a type `M` with multiplication, `z * (b * c) = z * b * c` holds true for all `b` and `c` in `M`.
|
Set.center_eq_univ
theorem Set.center_eq_univ : ∀ (M : Type u_1) [inst : CommSemigroup M], Set.center M = Set.univ
This theorem states that for any type `M` that has a `CommSemigroup` instance, the center of the magma of `M` is equal to the universal set of `M`. In mathematical terms, it asserts that in a commutative semigroup, every element is central, i.e., for all elements `x`, `y` in the semigroup, the equation `x*y=y*x` holds true.
More concisely: In a commutative semigroup, the center of the magma equals the universal set. That is, every element is central, i.e., for all `x, y` in the semigroup, `x * y = y * x`.
|
AddSemigroup.mem_center_iff
theorem AddSemigroup.mem_center_iff :
∀ {M : Type u_1} [inst : AddSemigroup M] {z : M}, z ∈ Set.addCenter M ↔ ∀ (g : M), g + z = z + g
This theorem states that for any type `M` with an addition operation (forming an additive semigroup), an element `z` of `M` is in the set of central elements (as defined by the `Set.addCenter` function) if and only if it commutes under addition with every element `g` of `M`. In other words, `z` is central if for every `g` in `M`, the equation `g + z = z + g` holds.
More concisely: For any additive semigroup `M`, an element `z` is in the center of `M` if and only if `z` commutes with every element `g` in `M`, i.e., `g + z = z + g` for all `g` in `M`.
|
IsMulCentral.right_assoc
theorem IsMulCentral.right_assoc :
∀ {M : Type u_1} [inst : Mul M] {z : M}, IsMulCentral z → ∀ (a b : M), a * b * z = a * (b * z)
This theorem states the associative property for right multiplication in terms of a central element in multiplication. Specifically, for any type `M` that supports multiplication (`Mul M`), given any central element `z` (`IsMulCentral z`), for any two elements `a` and `b` of type `M`, the equation `a * b * z = a * (b * z)` holds true. In other words, when multiplying `a`, `b`, and `z`, where `z` is a central element in the multiplication, the grouping of the multiplication does not change the result.
More concisely: For any type `M` with multiplication, and any central element `z` in `M`, the equation `a * b * z = a * (b * z)` holds for all `a, b` in `M`.
|
IsAddCentral.right_assoc
theorem IsAddCentral.right_assoc :
∀ {M : Type u_1} [inst : Add M] {z : M}, IsAddCentral z → ∀ (a b : M), a + b + z = a + (b + z)
This theorem states the associative property for right addition in the context of additive central elements. Specifically, for any type `M` that has a defined addition operation, any element `z` of `M` that is an additive central element, and any two elements `a` and `b` of `M`, the value of the expression `a + b + z` will be identical to the value of the expression `a + (b + z)`. In other words, when `z` is an additive central element, adding `z` to the sum of `a` and `b` is the same as adding `a` to the sum of `b` and `z`, demonstrating the associative property of this addition operation.
More concisely: For any additive central element `z` and elements `a`, `b` in an additive type `M`, the expression `a + b + z` equals `a + (b + z)`.
|
Semigroup.mem_center_iff
theorem Semigroup.mem_center_iff :
∀ {M : Type u_1} [inst : Semigroup M] {z : M}, z ∈ Set.center M ↔ ∀ (g : M), g * z = z * g
This theorem states that for any type `M` with a `Semigroup` structure and any element `z` of `M`, `z` is in the center of `M` if and only if for all elements `g` of `M`, the product of `g` and `z` is equal to the product of `z` and `g`. In other words, an element is in the center of a semigroup if it commutes with every other element in the semigroup.
More concisely: An element of a semigroup is in its center if and only if it commutes with every other element.
|
Set.inv_mem_center₀
theorem Set.inv_mem_center₀ :
∀ {M : Type u_1} [inst : GroupWithZero M] {a : M}, a ∈ Set.center M → a⁻¹ ∈ Set.center M
This theorem states that for any type `M` with a `GroupWithZero` structure, if an element `a` belongs to the center of `M` (i.e., it commutes with every other element in `M`), then its inverse `a⁻¹` also belongs to the center of `M`. In other words, if `a` is a central element in a group with zero, so is its inverse.
More concisely: If `a` is a central element in a group with zero `M`, then its inverse `a⁻¹` is also a central element in `M`.
|
IsAddCentral.left_assoc
theorem IsAddCentral.left_assoc :
∀ {M : Type u_1} [inst : Add M] {z : M}, IsAddCentral z → ∀ (b c : M), z + (b + c) = z + b + c
This theorem states the associative property for left addition of an element `z` in a type `M` that has an addition operation. Given that `z` is a central element under addition (`IsAddCentral z`), for any elements `b` and `c` in `M`, the sum of `z` and the sum of `b` and `c` (`z + (b + c)`) is equal to the sum of `z`, `b`, and `c` in sequence (`z + b + c`). In mathematical terms, it asserts that if `z` commutes with all elements under addition, then addition is associative with respect to `z` on the left.
More concisely: If `z` is a central element under addition in a commutative monoid `M`, then `z + (b + c)` equals `z + b + c` for all elements `b` and `c` in `M`.
|