Commit 2022-09-20 16:43 a5ed4088

View on Github →

feat(group_theory/coset): Construct the embedding H ⧸ ⨅ i, f i → Π i, H ⧸ f i (#16560) This PR constructs the embedding H ⧸ ⨅ i, f i → Π i, H ⧸ f i, which is needed for #16393.

Estimated changes