Commit 2022-05-04 17:58 aabcd895

chore(analysis/analytic_composition): weaken some typeclass arguments (#13924) There's no need to do a long computation to show the multilinear_map is bounded, when continuity follows directly from the definition. This deletes comp_along_composition_aux, and moves the lemmas about the norm of comp_along_composition further down the file so as to get the lemmas with weaker typeclass requirements out of the way first. The norm proofs are essentially unchanged.