mathlib

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

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(₂|₃)`