mathlib3
ab967d23 - feat(group_theory/submonoid): center of a submonoid (#8921)

Commit
4 years ago
feat(group_theory/submonoid): center of a submonoid (#8921) This adds `set.center`, `submonoid.center`, `subsemiring.center`, and `subring.center`, to complement the existing `subgroup.center`. This ran into a timeout, so had to squeeze some `simp`s in an unrelated file.
Author
Parents
Loading