basic): Action on an orbit (#9220)

Commit

4 years ago

feat(group_theory/group_action/basic): Action on an orbit (#9220) A `mul_action` restricts to a `mul_action` on an orbit.

Author

tb65536

Parents