mathlib

b2a65720 - feat(topology/instances/nnreal): generalize `has_continuous_smul` instance (#16713)

feat(topology/instances/nnreal): generalize `has_continuous_smul` instance (#16713) This generalizes the `has_continuous_smul ℝ≥0 ℝ` instance to `has_continuous_smul ℝ≥0 α` whenever there is a `mul_action ℝ α` with `has_continuous_smul R α` (the `mul_action` is the minimal assumption to get an induced action of `ℝ≥0` on `α` in mathlib).