feat(group_theory/coset): Embeddings of quotients (#10901)
feat(group_theory/coset): Embeddings of quotients (#10901)

If `K ≤ L`, then there is an embedding `K ⧸ (H.subgroup_of K) ↪ L ⧸ (H.subgroup_of L)`. Golfed from #9545.





leanprover-community/mathlib,leanprover-community/mathlib