English
If Ring.inverse is differentiable at invertible elements of a normed ring R (with summable geometric series), then it is differentiable everywhere on the set of units, and the derivative is -mulLeftRight 𝕜 R x^{-1} x^{-1}. In particular, hasStrictFDerivAt_inv' provides the derivative at x ≠ 0.
Русский
Если операция обратного в нормированном кольце R дифференцируема на множестве обратимых элементов, тогда она дифференцируема на множестве единиц и её производная равна -mulLeftRight 𝕜 R x^{-1} x^{-1}. В частности, hasStrictFDerivAt_inv' задаёт производную в x ≠ 0.
LaTeX
$$$\text{For } x \in R^{\times},\; HasStrictFDerivAt Ring.inverse (-mulLeftRight 𝕜 R x^{-1} x^{-1}) x.$$$
Lean4
@[fun_prop]
theorem differentiableAt_inverse {x : R} (hx : IsUnit x) : DifferentiableAt 𝕜 (@Ring.inverse R _) x :=
let ⟨u, hu⟩ := hx;
hu ▸ (hasFDerivAt_ringInverse u).differentiableAt
