mathlib3

14801617 - feat(group_theory/group_action/basic): Left multiplication satisfies the `quotient_action` axiom (#13249)

feat(group_theory/group_action/basic): Left multiplication satisfies the `quotient_action` axiom (#13249) This PR adds an instance `quotient_action α H`, meaning that left multiplication satisfies the `quotient_action` axiom.