Set.addCentralizer_eq_top_iff_subset
theorem Set.addCentralizer_eq_top_iff_subset :
∀ {M : Type u_1} {s : Set M} [inst : AddSemigroup M], s.addCentralizer = Set.univ ↔ s ⊆ Set.addCenter M
This theorem states that for any type `M`, which is an additive semigroup, and any subset `s` of `M`, the centralizer of `s` is equal to the universal set if and only if `s` is a subset of the center of `M`. Here, the centralizer of a set in an additive magma is the set of all elements that commute with every element of the original set, i.e., for any element `c` in the centralizer and `m` in the set, `m + c = c + m`. The center of an additive magma is the set of all elements that commute with every other element in the magma. The universal set is the set of all elements in a given type.
More concisely: For an additive semigroup M and subset s, the centralizer of s equals the universal set if and only if s is contained in the center of M.
|
Set.addCentralizer_univ
theorem Set.addCentralizer_univ : ∀ (M : Type u_1) [inst : AddSemigroup M], Set.univ.addCentralizer = Set.addCenter M
This theorem states that for any type `M` equipped with an addition operation (i.e., forming an additive semigroup), the centralizer of the universal set is equal to the center of `M`. In other words, the set of all elements in `M` that commute with every element in the universal set (i.e., satisfy `m + c = c + m` for all `m` in the universal set) is precisely the set of all elements in `M` that commute with every other element in `M`. This is essentially a statement about the commutativity of the addition operation in the entire `M`.
More concisely: The center of an additive semigroup equals its universal centralizer.
|
Set.centralizer_eq_top_iff_subset
theorem Set.centralizer_eq_top_iff_subset :
∀ {M : Type u_1} {s : Set M} [inst : Semigroup M], s.centralizer = Set.univ ↔ s ⊆ Set.center M
This theorem states that for any type `M`, any set `s` of type `M`, and any semigroup structure on `M`, the centralizer of `s` is equal to the universal set if and only if `s` is a subset of the center of `M`. Here, "centralizer" refers to the set of all elements in `M` that commute with every element in `s`, "universal set" refers to the set of all elements in `M`, and "center" refers to the set of all elements in `M` that commute with every other element in `M`. Essentially, the theorem states that all elements of `s` commute with all elements of `M` if and only if all elements of `s` are in the center of `M`.
More concisely: The centralizer of a subset `s` of type `M` equals the universal set if and only if `s` is contained in the center of `M`.
|
Set.centralizer_subset
theorem Set.centralizer_subset : ∀ {M : Type u_1} {S T : Set M} [inst : Mul M], S ⊆ T → T.centralizer ⊆ S.centralizer
This theorem states that for any type `M` with a multiplication operation and any two sets `S` and `T` of this type, if `S` is a subset of `T`, then the centralizer of `T` is a subset of the centralizer of `S`. Here, the centralizer of a set in a magma (a set with a single binary operation) is defined as the set of all elements in the magma such that each element when multiplied with any element from the set, the order of multiplication does not matter (i.e., `m * c = c * m` for all `m` in the set).
More concisely: If `S` is a subset of `T` in a magma `M` with multiplication operation, then the centralizer of `T` is contained in the centralizer of `S`.
|
Set.center_subset_centralizer
theorem Set.center_subset_centralizer : ∀ {M : Type u_1} [inst : Mul M] (S : Set M), Set.center M ⊆ S.centralizer := by
sorry
This theorem states that, for any type `M` equipped with a multiplication operation (represented by `Mul M`), and for any set `S` of elements of type `M`, the center of the magma `M` is a subset of the centralizer of the set `S`. In mathematical terms, this means that every element from the center of the magma (which is defined as those elements that commute with all other elements in the magma) also belongs to the centralizer of `S` (which is the set of all elements that commute with every element in `S`). Hence, every element in the center of the magma also commutes with every element in `S`.
More concisely: The center of a magma is a subset of its centralizer for any set of elements.
|
Set.mul_mem_centralizer
theorem Set.mul_mem_centralizer :
∀ {M : Type u_1} {S : Set M} {a b : M} [inst : Semigroup M],
a ∈ S.centralizer → b ∈ S.centralizer → a * b ∈ S.centralizer
This theorem states that for any type `M` that is a semigroup, if `a` and `b` are both elements of the centralizer of a set `S` of `M`, then the product of `a` and `b` is also an element of the centralizer of `S`. In other words, the centralizer of a set in a semigroup is closed under multiplication. This means that for all elements `m` in `S`, the equations `m * (a * b) = (a * b) * m` hold true, since `a * b` commutes with every element in `S`.
More concisely: In a semigroup, the centralizer of a set is closed under multiplication, i.e., if `a` and `b` are in the centralizer of a set `S`, then `a * b` is also in the centralizer of `S`.
|
Set.zero_mem_centralizer
theorem Set.zero_mem_centralizer : ∀ {M : Type u_1} (S : Set M) [inst : MulZeroClass M], 0 ∈ S.centralizer
This theorem states that for any type `M` that has both multiplication and a zero element (`MulZeroClass M`), and for any set `S` of elements of type `M`, the zero element is a member of the centralizer of `S`. The centralizer of a set in a magma is the set of elements that commute with every element of the original set. In mathematical terms, if `S` is a subset of a magma `M` with multiplication and a zero element, then for each element `m` in `S`, the equality `m * 0 = 0 * m` holds.
More concisely: For any magma `M` with a zero element and any subset `S` of `M` that is closed under multiplication, the zero element belongs to the centralizer of `S`.
|
Set.addCenter_subset_addCentralizer
theorem Set.addCenter_subset_addCentralizer :
∀ {M : Type u_1} [inst : Add M] (S : Set M), Set.addCenter M ⊆ S.addCentralizer
This theorem states that for any set `S` of a type `M` that has an addition operation (i.e., `M` is an additive magma), the center of `M` is a subset of the centralizer of `S`. In other words, every element in the center of the additive magma `M` (those elements `z` which commute with every element of `M` under addition) also belongs to the centralizer of the set `S` (those elements `c` for which, for every element `m` in `S`, addition of `m` and `c` commutes).
More concisely: For any additive magma `M` and subset `S` of `M`, the center of `M` is contained in the centralizer of `S`.
|
Set.centralizer_univ
theorem Set.centralizer_univ : ∀ (M : Type u_1) [inst : Semigroup M], Set.univ.centralizer = Set.center M
This theorem states that for any type `M` that forms a semigroup, the centralizer of the universal set is equal to the center of the magma. The centralizer of a set in a magma is the set of all elements that commute with every element of the original set. The universal set contains all elements of the type `M`. The center of a magma is the set of all elements that commute with every other element in the magma. Therefore, this theorem is essentially stating that every element in a semigroup that commutes with every other element is part of the center of the magma.
More concisely: In a semigroup, the centralizer of the universal set equals the center of the magma.
|