Commit 2022-10-28 07:08 549f9850

feat(analysis/calculus/cont_diff): norms of iterated derivatives (#17150) This PR adds four lemmas that calculate the norm of the (n+1)st iterated derivative as the left and right composition iterated_fderiv and fderiv with version for both iterated_fderiv and iterated_fderiv_within. While these lemmas are borderline trivial, they are very useful and finding linear_isometry_equiv.norm_map might be unintuitive.