mathlib

f4047663 - feat(analysis/normed_space/multilinear): add lemmas/defs (#19114)

feat(analysis/normed_space/multilinear): add lemmas/defs (#19114) * Add `simps` here and there. * Add `continuous_multilinear_map.norm_of_subsingleton_le` and `continuous_multilinear_map.nnnorm_of_subsingleton_le`. * Add `continuous_multilinear_map.cod_restrict`. * Add `continuous_multilinear_map.restrict_scalarsₗᵢ`, a `linear_isometry_equiv` version of `continuous_multilinear_map.restrict_scalars`. * Split `continuous_multilinear_map.dom_dom_congr` into 3 definitions: a map, an equivalence, and a linear isometry (the old def).