# 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.