Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-03 16:02 bb15b1ce

View on Github →

chore(analysis/calculus): rename has_f?deriv_at_unique to has_f?deriv_at.unique (#6019) Also make some lemmas protected.

Estimated changes

added theorem has_deriv_at.unique
deleted theorem has_deriv_at_unique
deleted theorem linear_map.deriv
deleted theorem linear_map.deriv_within
deleted theorem linear_map.has_deriv_at
added theorem has_fderiv_at.unique
deleted theorem has_fderiv_at_unique