mathlib

01788b5e - feat(group_theory/subgroup/basic): add some trivial lemmas (#16915)

feat(group_theory/subgroup/basic): add some trivial lemmas (#16915) * add `subgroup.subtype_injective`, `subgroup.le_closure_to_submonoid`, `subgroup.closure_eq_top_of_mclosure_eq_top`; * golf `subgroup.closure_inv`, `subgroup.map_le_map_iff_of_injective`, and `subgroup.map_injective`.