Commit 2024-11-06 14:51 5f6f83e2

View on Github →

feat: the Faa di Bruno formula (#17400)

Estimated changes

Modified Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean

added def FormalMultilinearSeries.compAlongOrderedFinpartition

added theorem FormalMultilinearSeries.compAlongOrderedFinpartition_apply

added theorem HasFTaylorSeriesUpToOn.comp

added def OrderedFinpartition.applyOrderedFinpartition

added theorem OrderedFinpartition.applyOrderedFinpartition_apply

added theorem OrderedFinpartition.applyOrderedFinpartition_update_left

added theorem OrderedFinpartition.applyOrderedFinpartition_update_right

added theorem OrderedFinpartition.compAlongOrderFinpartition_apply

added def OrderedFinpartition.compAlongOrderedFinpartition

added theorem OrderedFinpartition.compAlongOrderedFinpartitionL_apply

added def OrderedFinpartition.compAlongOrderedFinpartitionₗ

added theorem analyticOn_taylorComp