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
.