bundled sets closed under a mul action #4996

Stream: PR reviews

[Johan Commelin]

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]

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

[Eric Wieser]

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.