mathlib3

4db21255 - feat(group_theory/submonoid): add `*.of_mclosure_eq_top` (#16985)

feat(group_theory/submonoid): add `*.of_mclosure_eq_top` (#16985) * add `is_scalar_tower.of_mclosure_eq_top` and `smul_comm_class.of_mclosure_eq_top`; * golf `submonoid.closure_comm_monoid_of_comm`; * add `con.mrange_mk'`.