cont_diff): formula for iterated derivative of composition with linear maps (#18592)

Commit

2 years ago

feat(analysis/calculus/cont_diff): formula for iterated derivative of composition with linear maps (#18592) And missing API for derivatives and iterated derivatives.

Author

sgouezel

Parents

290a7ba0

mathlib3 4601791e - feat(analysis/calculus/cont_diff): formula for iterated derivative of composition with linear maps (#18592)

mathlib3
4601791e - feat(analysis/calculus/cont_diff): formula for iterated derivative of composition with linear maps (#18592)