mathlib3

c6c7eaf3 - refactor(topology/algebra/module,analysis/*): merge some `smul` lemmas and defs (#5987)

refactor(topology/algebra/module,analysis/*): merge some `smul` lemmas and defs (#5987) Generalize some definitions and lemmas about `smul` and `f : E →L[k] F` so that now they allow scalars from an algebra over `k`. This way we can get rid of `smul_algebra` definitions and lemmas. In particular, now `continuous_linear_map.smul_right` accepts functions with values in an algebra over `k`, so `smul_right 1 f` now needs a type annotation on `1`.