Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subgroup.quotient_subgroup_of_embedding_of_le_apply_mk

Modification history

2022-09-20 16:43
src/group_theory/coset.lean
feat(group_theory/coset): Construct the embedding `H ⧸ ⨅ i, f i → Π i, H ⧸ f i` (#16560) …
Added subgroup.quotient_subgroup_of_embedding_of_le_apply_mkView on Github →