Commit 2023-06-22 02:23 f4047663

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).