Zulip Chat Archive

Stream: PR reviews

Topic: bundled sets closed under a mul action #4996


Johan Commelin (Nov 27 2020 at 07:16):

Eric Wieser created this PR. I think it's useful. There is some discussion about the name.
So the question is: how should we call a bundled set closed under a mul_action.

Johan Commelin (Nov 27 2020 at 07:18):

/poll Name for a bundled (set that is closed under a mul_action)
sub_mul_action
mul_subaction
closed_subset

Eric Wieser (Nov 27 2020 at 12:12):

At some point I'd like to follow up with a structure sub_action_and_monoid [algebra R A] extends submonoid A, submul_action R A, for submonoids of an algebra which include the base ring - it would be nice if whatever name we pick in this thread leaves me a clear choice for the name to use for that.


Last updated: Dec 20 2023 at 11:08 UTC