mathlib

d3af0609 - chore(analysis/normed_space/basic): introduce `norm_smul_le` (#18650)

chore(analysis/normed_space/basic): introduce `norm_smul_le` (#18650) Currently `norm_smul_le x y` is just a special case of `(norm_smul x y).le`; but if in future we generalize `normed_space` to work over normed rings, it will continue to hold where `norm_smul` no longer does. This adjusts downstream proofs to use the weaker lemma too when the stronger one isn't needed, both so that we have less to fix if/when we make the suggested refactor, and because the new spelling is shorter. This adds the corresponding `nnnorm` and `dist` and `nndist` lemmas too.