Commit 2022-10-25 07:35 a4c2bd4a

feat(group_theory/coset): Add the embedding α ⧸ (⨅ i, f i) → Π i, α ⧸ f i (#16658) Mathlib already has the relative version H ⧸ (⨅ i, f i).subgroup_of H → Π i, H ⧸ (f i).subgroup_of H, but the absolute version is also useful and can be proved similarly.