mathlib

aa68866e - feat(analysis/calculus/cont_diff): bound for the n-th derivative of a composition (#18643)

feat(analysis/calculus/cont_diff): bound for the n-th derivative of a composition (#18643) We prove the bound `n! * C * D^n` for the `n`-th derivative of `g ∘ f` if the derivatives of `g` are bounded by `C` and the `i`-th derivative of `f` is bounded by `D^i`.