mathlib3

171e2aa2 - feat(group_theory/group_action/basic): A `quotient_action` induces an action on left cosets (#13283)