Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-23 15:31 81f6e887

View on Github →

chore(analysis/calculus): add 2 simple lemmas (#9334) Add differentiable_on.has_fderiv_at and differentiable_on.has_deriv_at.

Estimated changes