Centers of monoids #
Main definitions #
Submonoid.center
: the center of a monoidAddSubmonoid.center
: the center of an additive monoid
We provide Subgroup.center
, AddSubgroup.center
, Subsemiring.center
, and Subring.center
in
other files.
The center of a monoid M
is the set of elements that commute with everything in M
Instances For
The center of a monoid M
is the set of elements that commute with everything in M
Instances For
The center of a monoid is commutative.
The center of a monoid acts commutatively on that monoid.
The center of a monoid acts commutatively on that monoid.
Note that smulCommClass (center M) (center M) M
is already implied by
Submonoid.smulCommClass_right
For an additive monoid, the units of the center inject into the center of the units.
Instances For
For a monoid, the units of the center inject into the center of the units. This is not an
equivalence in general; one case when it is is for groups with zero, which is covered in
centerUnitsEquivUnitsCenter
.