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
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: Aug 03 2023 at 10:10 UTC