Theorem HasDerivAtFilter.sum

Modification history

2026-02-18 03:15

Mathlib/Analysis/Calculus/Deriv/Add.lean

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

Modified HasDerivAtFilter.sum View on Github →

2023-05-28 08:49

Mathlib/Analysis/Calculus/Deriv/Add.lean

feat: port Analysis.Calculus.Deriv.Add (#4435)

Added HasDerivAtFilter.sum View on Github →