Structure HasStrictFDerivAt

Modification history

2024-11-15 20:51

Mathlib/Analysis/Calculus/FDeriv/Basic.lean

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

Added HasStrictFDerivAt View on Github →