mathlib3

165e0556 - refactor(group_theory/quotient_group): use `con` (#10699)

refactor(group_theory/quotient_group): use `con` (#10699) Use `con` to define `group` structure on `G ⧸ N` instead of repeating the construction in this case.