Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-19 08:28 28a360a6

View on Github →

feat(analysis/calculus/deriv): prove deriv_inv at x = 0 as well (#8748)

  • turn differentiable_at_inv and differentiable_at_fpow into iff lemmas;
  • slightly weaker assumptions for differentiable_within_at_fpow etc;
  • prove deriv_inv and fderiv_inv for all x;
  • prove formulas for iterated derivs of x⁻¹ and x ^ m, m : int;
  • push coe in these formulas;

Estimated changes

added theorem deriv_fpow'
modified theorem deriv_fpow
added theorem deriv_inv''
modified theorem deriv_inv'
modified theorem deriv_inv
modified theorem deriv_within_fpow
modified theorem differentiable_at_fpow
modified theorem differentiable_at_inv
modified theorem differentiable_on_fpow
modified theorem fderiv_inv
modified theorem has_deriv_at_fpow
modified theorem has_deriv_within_at_fpow
modified theorem has_strict_deriv_at_fpow
added theorem iter_deriv_fpow'
modified theorem iter_deriv_fpow
added theorem iter_deriv_inv'
added theorem iter_deriv_inv
modified theorem iter_deriv_pow'
modified theorem iter_deriv_pow