Commit 2023-01-13 10:23 cf8e77c6

View on Github →

feat(group_theory/subgroup/basic): Map a subgroup under an iso (#17775) Cross-reference mul_equiv.subgroup_map and subgroup.equiv_map_of_injective. Add lemmas connecting them.

Estimated changes

Modified src/group_theory/commensurable.lean

Modified src/group_theory/subgroup/basic.lean

added theorem mul_equiv.coe_subgroup_map_apply

modified def mul_equiv.subgroup_map

added theorem mul_equiv.subgroup_map_symm_apply

modified theorem subgroup.comap_injective_is_commutative

added theorem subgroup.equiv_map_of_injective_coe_mul_equiv

Modified src/group_theory/submonoid/operations.lean

added theorem mul_equiv.coe_submonoid_map_apply

added theorem mul_equiv.submonoid_map_symm_apply

added theorem submonoid.equiv_map_of_injective_coe_mul_equiv