Centralizers in semigroups, as subsemigroups. #
Main definitions #
Subsemigroup.centralizer
: the centralizer of a subset of a semigroupAddSubsemigroup.centralizer
: the centralizer of a subset of an additive semigroup
We provide Monoid.centralizer
, AddMonoid.centralizer
, Subgroup.centralizer
, and
AddSubgroup.centralizer
in other files.
The centralizer of a subset of a semigroup M
.
Equations
Instances For
The centralizer of a subset of an additive semigroup.
Instances For
@[simp]
@[simp]
instance
AddSubsemigroup.decidableMemCentralizer
{M : Type u_1}
{S : Set M}
[AddSemigroup M]
(a : M)
[Decidable (∀ b ∈ S, b + a = a + b)]
:
Decidable (a ∈ centralizer S)
@[simp]
@[simp]
theorem
AddSubsemigroup.closure_le_centralizer_centralizer
{M : Type u_1}
[AddSemigroup M]
(s : Set M)
:
@[reducible, inline]
abbrev
AddSubsemigroup.closureAddCommSemigroupOfComm
(M : Type u_1)
[AddSemigroup M]
{s : Set M}
(hcomm : ∀ a ∈ s, ∀ b ∈ s, a + b = b + a)
:
AddCommSemigroup ↥(closure s)
If all the elements of a set s
commute, then closure s
forms an additive
commutative semigroup.