differentiableAt_inv — Mathlib

English

If x is a unit, then the map Inv.inv is differentiable at x with derivative given by -mulLeftRight 𝕜 R x^{-1} x^{-1}.

Русский

Если x является единицей, то Inv.inv дифференцируема в x с производной -mulLeftRight 𝕜 R x^{-1} x^{-1}.

LaTeX

$$$\text{DifferentiableAt } Inv.inv x = -mulLeftRight 𝕜 R x^{-1} x^{-1}$$$

Lean4

@[fun_prop]
theorem differentiableAt_inv {x : R} (hx : x ≠ 0) : DifferentiableAt 𝕜 Inv.inv x :=
  (hasFDerivAt_inv' hx).differentiableAt

Похожие утверждения