Mathlib v3 is deprecated. Go to Mathlib v4

Def subgroup.quotient_subgroup_of_map_of_le

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_map_of_leView on Github →