Theorem fderivWithin_zero_of_not_uniqueDiffWithinAt

Modification history

2026-04-23 19:18
Mathlib/Analysis/Calculus/FDeriv/Basic.lean
feat(Analysis/Calculus/IteratedDeriv): add affine composition lemmas (#36357) …
Added fderivWithin_zero_of_not_uniqueDiffWithinAtView on Github →