Bundled `sub*` and `center`

Stream: general

[Yury G. Kudryashov]

How should we handle, e.g., center once we'll have bundled submonoid, subgroup, subring, subalgebra, ...? Should it be sub*.center with lemmas like subgroup.center.to_submonoid = submonoid.center? Or should we continue using center M : set M with [is_sub* (center M)]? Something else?

[Yury G. Kudryashov]

Similar question about, e.g., mul_action.restrict [mul_action M α] (s : set M) [is_submonoid s] : mul_action s α.