Commit 2020-05-17 07:42 b530cdb4
View on Github →refactor(normed_space): require norm_smul_le
instead of norm_smul
(#2693)
While in many cases we can prove norm_smul
directly, in some cases (e.g., for the operator norm) it's easier to prove norm_smul_le
. Redefine normed_space
to avoid repeating the same trick over and over.