Def HasStrictFDerivAt

Modification history

2026-02-18 03:15

Mathlib/Analysis/Calculus/FDeriv/Defs.lean

refactor(Analysis/Calculus): redefine `HasFDerivAtFilter` (#34965) …

Added HasStrictFDerivAt View on Github →

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 →