mathlib

90dc6175 - feat(analysis/calculus/cont_diff): `iterated_fderiv[_within]` is linear in the function (#15902)

feat(analysis/calculus/cont_diff): `iterated_fderiv[_within]` is linear in the function (#15902) This PR adds lemmas for calculating the iterated Fréchet-derivative of addition, negation, and constant scalar multiplication. For each operation, we provide two lemmas, one for `iterated_fderiv_within` and on for `iterated_fderiv`. Co-authored-by: Moritz Doll <moritz.doll@googlemail.com> Co-authored-by: mcdoll <moritz.doll@googlemail.com>