mathlib

b02e2ea1 - 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.