mathlib

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

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;