basic): `subgroup.map_le_map_iff_of_injective` (#11947)

Commit

4 years ago

feat(group_theory/subgroup/basic): `subgroup.map_le_map_iff_of_injective` (#11947) If `f` is injective, then `H.map f ≤ K.map f ↔ H ≤ K`.

Author

tb65536

Parents