Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subsemigroup.center_eq_top

Modification history

2023-06-14 10:32
src/group_theory/subsemigroup/center.lean
chore(*): fix `@[to_additive, simp]` to the correct order (#19169) …
Modified subsemigroup.center_eq_topView on Github →
2022-05-10 03:35
src/group_theory/subsemigroup/center.lean
feat(group_theory/subsemigroup/{center, centralizer}): define center and centralizer as subsemigroups (#13627) …
Added subsemigroup.center_eq_topView on Github →