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.