mathlib3

1f195436 - feat(topology/algebra/group): `•` lemmas (#17383)

feat(topology/algebra/group): `•` lemmas (#17383) Write the `smul` version of several `mul` lemmas, along with the missing instance `has_continuous_mul M M → has_continuous_smul Mᵐᵒᵖ M`