Stream: PR reviews
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
Johan Commelin (Nov 27 2020 at 07:18):
/poll Name for a bundled (set that is closed under a mul_action)
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