Commit 2022-10-12 07:21 01788b5e

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.