mathlib3

dced1336 - feat(group_theory/group_action/basic): Right multiplication satisfies the `quotient_action` axiom (#13475)