# Commit 2021-02-05 12:11 c6c7eaf3

View on Github →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`

.