Def lie_submodule.quotient.mk'

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

feat(linear_algebra/basic, group_theory/quotient_group, algebra/lie/quotient): ext lemmas for morphisms out of quotients (#8641) …