Commit 2025-12-02 22:00 93892696

View on Github →

feat: iteratedDeriv_const and iteratedDerivWithin_const (#32366)

Estimated changes

Modified Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean

added theorem iteratedDerivWithin_const

added theorem iteratedDeriv_const