Theorem hasFDerivWithinAt_diff_singleton_self

Modification history

2026-06-09 08:51
Mathlib/Analysis/Calculus/FDeriv/Basic.lean
chore: rename `diff` to `sdiff` (#40184) …
Deleted hasFDerivWithinAt_diff_singleton_selfView on Github →
2026-02-04 18:01
Mathlib/Analysis/Calculus/FDeriv/Basic.lean
feat(FDeriv/Congr): generalize to TVS (#34843)
Added hasFDerivWithinAt_diff_singleton_selfView on Github →