mathlib3

108e3a07 - refactor(group_theory/coset): redefine quotient group to be quotient by action of subgroup (#15045)

refactor(group_theory/coset): redefine quotient group to be quotient by action of subgroup (#15045) Given a group `α` and subgroup `s`, redefine the relation `left_rel` ("being in the same left coset") to ```lean def left_rel : setoid α := mul_action.orbit_rel s.opposite α ``` This means that a quotient group is definitionally a quotient by a group action. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/two.20different.20quotients.20by.20subgroup)