Commit 2020-05-17 07:42 b530cdb4

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.