mathlib

c5e0299a - feat(group_theory/subsemigroup/{center, centralizer}): define center and centralizer as subsemigroups (#13627)

feat(group_theory/subsemigroup/{center, centralizer}): define center and centralizer as subsemigroups (#13627) This defines the center and centralizers for semigroups. This is necessary so that we can do the same for non-unital semirings. - [x] depends on: #12112 - [x] depends on: #13903