mathlib

17b3357b - feat(topology/algebra): generalize `has_continuous_smul` arguments to `has_continuous_const_smul` (#11999)

feat(topology/algebra): generalize `has_continuous_smul` arguments to `has_continuous_const_smul` (#11999) This changes the majority of the downstream call-sites of the `const_smul` lemmas to only need the weaker typeclass.