mathlib

3b91c324 - feat(group_theory/subgroup/basic): `map_le_map_iff_of_injective` for `subtype` (#12713)

feat(group_theory/subgroup/basic): `map_le_map_iff_of_injective` for `subtype` (#12713) This PR adds the special case of `map_le_map_iff_of_injective` when the group homomorphism is `subtype`. This is useful when working with nested subgroups. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>