mathlib3

35bc69bc - feat(group_theory/subgroup): add several trivial lemmas (#16633)

feat(group_theory/subgroup): add several trivial lemmas (#16633) * add `subgroup.top_to_submonoid` and `subgroup.bot_to_submonoid`; * add `free_monoid.mrange_lift`.