Commit 2024-02-20 08:45 73c0d3b2

View on Github →

feat: Basic theorems for iteratedFDerivWithin (#10733) Basic theorems for iteratedFDerivWithin

Estimated changes

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

added theorem iteratedFDerivWithin_const_of_ne

added theorem iteratedFDerivWithin_succ_const

added theorem iteratedFDerivWithin_sum_apply

added theorem iteratedFDerivWithin_zero_fun

added theorem iteratedFDeriv_sum

modified theorem iteratedFDeriv_zero_fun