Def quotient_group.ker_lift

feat(*): `A ⧸ B` notation for quotients in algebra (#10501) …

chore(group_theory/*): refactor quotient groups to use bundled subgroups (#3321)

feat(group_theory/quotient_group): define ker_lift and prove simp-lemmas (#764) …