Commit 2022-09-20 16:43 a5ed4088

View on Github →

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.

Estimated changes

Modified src/group_theory/coset.lean

added def subgroup.quotient_infi_embedding

added theorem subgroup.quotient_infi_embedding_apply_mk

modified def subgroup.quotient_subgroup_of_embedding_of_le

added theorem subgroup.quotient_subgroup_of_embedding_of_le_apply_mk

added def subgroup.quotient_subgroup_of_map_of_le

added theorem subgroup.quotient_subgroup_of_map_of_le_apply_mk