Centralizers of magmas and monoids #
Main definitions #
Submonoid.centralizer
: the centralizer of a subset of a monoidAddSubmonoid.centralizer
: the centralizer of a subset of an additive monoid
We provide Subgroup.centralizer
, AddSubgroup.centralizer
in other files.
The centralizer of a subset of an additive monoid.
Equations
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[reducible, inline]
abbrev
Submonoid.closureCommMonoidOfComm
(M : Type u_1)
[Monoid M]
{s : Set M}
(hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a)
:
CommMonoid ↥(closure s)
If all the elements of a set s
commute, then closure s
is a commutative monoid.
Equations
Instances For
@[reducible, inline]
abbrev
AddSubmonoid.closureAddCommMonoidOfComm
(M : Type u_1)
[AddMonoid M]
{s : Set M}
(hcomm : ∀ a ∈ s, ∀ b ∈ s, a + b = b + a)
:
AddCommMonoid ↥(closure s)
If all the elements of a set s
commute, then closure s
forms an additive
commutative monoid.