Theorem hasDerivAtFilter_zero

Modification history

2026-02-18 03:15

Mathlib/Analysis/Calculus/Deriv/Basic.lean

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

Modified hasDerivAtFilter_zero View on Github →

2025-03-31 08:28

Mathlib/Analysis/Calculus/Deriv/Basic.lean

feat(Analysis/Calculus): lemmas about derivatives of constant functions (#23310) …

Added hasDerivAtFilter_zero View on Github →