Zulip Chat Archive

Stream: general

Topic: Bundled `sub*` and `center`

Yury G. Kudryashov (Feb 15 2020 at 20:52):

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 (Feb 15 2020 at 20:53):

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

Last updated: Dec 20 2023 at 11:08 UTC