Commit 2024-01-17 17:22 9c832bc4

feat(Analysis/NormedSpace/{ProdLp,PiLp}): add BoundedSMul instances (#9796) Also adds:

• Lemmas linking the $L^\infty$ norm via WithLp to the standard one on products
• A new BoundedSMul.of_nnnorm_smul_le which eliminates all the positivity juggling. In theory we could generalize even further to non-unital rings, but that would require more generalization of WithLp, and is trivial for someone to do later; the proofs here will still work.