Theorem iteratedDerivWithin_neg'

Modification history

2025-06-25 15:59
Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
chore: add `fun_` versions in the files on one-dimensional derivatives (#26355) …
Deleted iteratedDerivWithin_neg'View on Github →
2024-03-07 15:45
Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
feat: generalize some lemmas about iterated derivatives (#11213)
Modified iteratedDerivWithin_neg'View on Github →
2024-01-19 09:25
Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
feat: add lemmas about iteratedDerivWithin (#9679) …
Added iteratedDerivWithin_neg'View on Github →