Commit 2023-03-25 15:44 d3af0609

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.