English
If x ≠ 0, the derivative at x of the map t ↦ t^{-1} is the linear map that sends a direction h to −h/x^2, i.e., HasFDerivAt (x^{-1}) is the smulRight map by −(x^2)^{-1}.
Русский
Если x ≠ 0, производная в точке x от отображения t ↦ t^{-1} — это линейное отображение, отправляющее направление h в −h/x^2, то есть HasFDerivAt (x^{-1}) равна умножению на −(x^2)^{-1}.
LaTeX
$$$\\forall 𝕜 [NontriviallyNormedField 𝕜], x \\ne 0 \\Rightarrow HasFDerivAt (\\lambda t. t^{-1}) (smulRight (1 : 𝕜 \\toL[𝕜] 𝕜) (-(x^2)^{-1}) ) x$$$
Lean4
theorem hasFDerivAt_inv (x_ne_zero : x ≠ 0) :
HasFDerivAt (fun x => x⁻¹) (smulRight (1 : 𝕜 →L[𝕜] 𝕜) (-(x ^ 2)⁻¹) : 𝕜 →L[𝕜] 𝕜) x :=
hasDerivAt_inv x_ne_zero
