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 a monoid M
.
Equations
- Submonoid.centralizer S = { carrier := S.centralizer, mul_mem' := ⋯, one_mem' := ⋯ }
Instances For
The centralizer of a subset of an additive monoid.
Equations
- AddSubmonoid.centralizer S = { carrier := S.addCentralizer, add_mem' := ⋯, zero_mem' := ⋯ }
Instances For
@[simp]
@[simp]
@[simp]
@[simp]