mathlib3

cf8e77c6 - feat(group_theory/subgroup/basic): Map a subgroup under an iso (#17775)

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.