mathlib3

b530cdb4 - refactor(normed_space): require `norm_smul_le` instead of `norm_smul` (#2693)

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. Co-authored-by: Heather Macbeth <hrmacbeth@users.noreply.github.com> Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>