Theorem HasFDerivAt.eventually_ne

Modification history

2026-02-10 19:29
Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
feat(Analysis/Calculus/Deriv/Inverse): add `deriv_zero_of_frequently_mem` (#34576) …
Modified HasFDerivAt.eventually_neView on Github →
2023-05-22 19:15
Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
feat: port Analysis.Calculus.Fderiv.Equiv (#4210)
Added HasFDerivAt.eventually_neView on Github →