Def HasStrictFDerivAt

Modification history

2024-11-15 20:51

Mathlib/Analysis/Calculus/FDeriv/Basic.lean

refactor: make `HasStrictFDerivAt` a structure (#19104) …

Deleted HasStrictFDerivAt View on Github →

2023-05-21 21:51

Mathlib/Analysis/Calculus/FDeriv/Basic.lean

feat: port Analysis.Calculus.FDeriv.Basic (#4132)

Added HasStrictFDerivAt View on Github →