Theorem DifferentiableWithinAt.of_insert

Modification history

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