Zulip Chat Archive

Stream: PR reviews

Topic: bundled sets closed under a mul action #4996


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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: May 06 2021 at 11:23 UTC