Commit 2023-05-22 17:42 f32d52b6

View on Github →

chore: fix a name, protect (#4212)

Rename ContinuousLinearMap.hasStrictFderivAt to ContinuousLinearMap.hasStrictFDerivAt.
Protect some theorems in Analysis/Calculus/FDeriv/Basic.

Estimated changes

Modified Mathlib/Analysis/Calculus/FDeriv/Basic.lean

deleted theorem DifferentiableAt.fderivWithin

deleted theorem HasCompactSupport.fderiv

deleted theorem HasFDerivAt.fderiv

deleted theorem HasFDerivWithinAt.fderivWithin

deleted theorem HasFDerivWithinAt.nhdsWithin

Modified Mathlib/Analysis/Calculus/FDeriv/Linear.lean