Commit 2024-11-28 16:12 e71723be

feat: Goursat's lemma for subgroups (#18823) Proves Goursat's lemma for subgroups. If I is a subgroup of G × H which projects fully on both factors, then there exist normal subgroups G' ≤ G and H' ≤ H such that G' × H' ≤ I and the image of I in G ⧸ G' × H ⧸ H' is the graph of an isomorphism G ⧸ G' ≃ H ⧸ H'. We construct G' and H' as explicit subgroups.