Commit 2022-05-10 03:35 c5e0299a

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.

• depends on: #12112
• depends on: #13903