Commit 2021-12-20 11:53 b02e2ea1
View on Github →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.
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.