mathlib3

549f9850 - feat(analysis/calculus/cont_diff): norms of iterated derivatives (#17150)

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.