mathlib

a4c2bd4a - feat(group_theory/coset): Add the embedding `α ⧸ (⨅ i, f i) → Π i, α ⧸ f i` (#16658)

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.