Theorem hasFDerivWithinAt_diff_singleton_self

Modification history

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 →