mathlib3

92d019a0 - feat(group_theory/coset): Construct the embedding `H ⧸ ⨅ i, f i → Π i, H ⧸ f i` (#16560)

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. Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>