Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-16 18:36 b0071f3f

View on Github →

feat(analysis/special_functions): sqrt is infinitely smooth at x ≠ 0 (#6255) Also move lemmas about differentiability of sqrt out from special_functions/pow to a new file.

Estimated changes

added theorem times_cont_diff_at.pow
added theorem times_cont_diff_on.pow
deleted theorem deriv_sqrt
deleted theorem deriv_within_sqrt
deleted theorem differentiable.sqrt
deleted theorem differentiable_at.sqrt
deleted theorem differentiable_on.sqrt
deleted theorem has_deriv_at.sqrt
deleted theorem has_deriv_within_at.sqrt
added theorem deriv_sqrt
added theorem deriv_within_sqrt
added theorem differentiable.sqrt
added theorem differentiable_at.sqrt
added theorem differentiable_on.sqrt
added theorem fderiv_sqrt
added theorem fderiv_within_sqrt
added theorem has_deriv_at.sqrt
added theorem has_fderiv_at.sqrt
added theorem measurable.sqrt
added theorem real.deriv_sqrt_aux
added theorem real.has_deriv_at_sqrt
added theorem times_cont_diff.sqrt