Commit 2023-12-27 13:14 6ecca6c4

feat(GroupTheory/GroupAction/Opposite): add notation for right and left actions (#8909) The new notations (with open scoped RightActions) are:

• r •> m as an alias for r • m
• m <• r as an alias for MulOpposite.op r • m
• r +ᵥ> m as an alias for r +ᵥ m
• m <+ᵥ r as an alias for AddOpposite.op r +ᵥ m An alternative proposal was to use variants of • with arrows inside:
• r ⮊ m as an alias for r • m
• m ⮈ r as an alias for MulOpposite.op r • m but this doesn't have an obvious additive counterpart, and apparently has font issues. Zulip messages:
• "And m <• r would be notation for (to_opposite r) • m, or something like that?"
• "I rather like the idea of having a new piece of notation for right actions"
• I like your proposed notation <• for the right scalar action. Maybe we should even introduce •> as an alias for •