Mathlib v3 is deprecated. Go to Mathlib v4

Theorem has_deriv_at.tendsto_punctured_nhds

Modification history

2023-05-27 19:40
src/analysis/calculus/deriv.lean
chore(analysis/calculus/deriv): split file (#19113) …
Modified has_deriv_at.tendsto_punctured_nhdsView on Github →
2021-12-18 14:23
src/analysis/calculus/deriv.lean
feat(analysis/calculus/deriv): add `has_deriv_at.tendsto_punctured_nhds` (#10877)
Added has_deriv_at.tendsto_punctured_nhdsView on Github →