mathlib3

1432c308 - feat(topology/algebra/mul_action): `λ x, c • x` is a closed map for all `c` (#9756)

feat(topology/algebra/mul_action): `λ x, c • x` is a closed map for all `c` (#9756) * rename old `is_closed_map_smul₀` to `is_closed_map_smul_of_ne_zero`; * add a new `is_closed_map_smul₀` that assumes more about typeclasses but works for `c = 0`.