Centralizers of magmas and monoids #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
Main definitions #
add_subgroup.centralizer in other files.
The centralizer of a subset of a monoid
The centralizer of a subset of an additive monoid.