Commit 2022-09-30 08:02 b2a65720

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).