Commit 2022-06-29 20:38 108e3a07
View on Github →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
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