Theorem hasFDerivWithinAt_insert_self

Modification history

2026-02-04 18:01
Mathlib/Analysis/Calculus/FDeriv/Basic.lean
feat(FDeriv/Congr): generalize to TVS (#34843)
Added hasFDerivWithinAt_insert_selfView on Github →