Structure HasStrictFDerivAt

Modification history

2025-05-27 02:03

Mathlib/Analysis/Calculus/FDeriv/Basic.lean

chore(Analysis/Calculus): split long file FDeriv/Basic.lean (#25207)

Modified HasStrictFDerivAt View on Github →

2024-11-15 20:51

Mathlib/Analysis/Calculus/FDeriv/Basic.lean

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

Added HasStrictFDerivAt View on Github →