Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-18 14:23 65118e5f

View on Github →

feat(analysis/calculus/deriv): add has_deriv_at.tendsto_punctured_nhds (#10877)

Estimated changes