Commit 2022-05-04 17:58 aabcd895
View on Github →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.