Commit 2022-06-05 14:52 043fa29d

feat(src/analysis/normed_space): various improvements for continuous bilinear maps (#14539)

• Add simps to arrow_congrSL
• continuous_linear_map.flip (compSL F E H σ₂₁ σ₁₄) takes almost 5 seconds to elaborate, but when giving the argument (F →SL[σ₂₄] H) for G explicitly, this goes down to 1 second.
• Reorder arguments of is_bounded_bilinear_map_comp
• Use continuous_linear_map results to prove is_bounded_bilinear_map results.
• Make arguments to comp_continuous_multilinear_mapL explicit
• Add continuous[_on].clm_comp, cont_diff[_on].clm_comp and cont_diff.comp_cont_diff_on(₂|₃)