mathlib3

83bd2e68 - feat(analysis/normed_space/multilinear): add a few inequalities (#8018)

feat(analysis/normed_space/multilinear): add a few inequalities (#8018) Also add a few lemmas about `tsum` and `nnnorm`. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>