mathlib

769ec8c8 - feat(group_theory/group_action/basic): Right multiplication satisfies the `quotient_action` axiom (#13362)

feat(group_theory/group_action/basic): Right multiplication satisfies the `quotient_action` axiom (#13362) This PR adds an instance stating that the right multiplication action of `H.normalizer.opposite` on `G` satisfies the `quotient_action` axiom. In particular, we automatically get the induced action of `H.normalizer.opposite` on `G ⧸ H`, so we can delete the existing instance. (Technically, the existing instance was stated in terms of `H.normalizerᵐᵒᵖ`, but I think `H.normalizer.opposite` is a more natural way to write it).