English
Same as above: if differentiable at x and x ≠ 0, then derivative of inverse is − derivAt x / x^2.
Русский
Как выше: если дифференцируемо в x и x ≠ 0, тогда производная обратной функции − deriv x / x^2.
LaTeX
$$$\\text{If } hc: DifferentiableAt 𝕜 c x \\text{ and } hx: c x ≠ 0, \\text{ then } deriv (c^{-1}) x = - (deriv c x)/c x^2$$$
Lean4
@[simp]
theorem deriv_inv'' (hc : DifferentiableAt 𝕜 c x) (hx : c x ≠ 0) : deriv (c⁻¹) x = -deriv c x / c x ^ 2 :=
(hc.hasDerivAt.inv hx).deriv