mathlib

329393a7 - feat(analysis/calculus/times_cont_diff): iterated smoothness in terms of deriv (#4017)

feat(analysis/calculus/times_cont_diff): iterated smoothness in terms of deriv (#4017) Currently, iterated smoothness is only formulated in terms of the Fréchet derivative. For one-dimensional functions, it is more handy to use the one-dimensional derivative `deriv`. This PR provides a basic interface in this direction.