fderiv_inv' — Mathlib

English

In a noncommutative normed division ring R, the Fréchet derivative of the map x ↦ x^{-1} at x ≠ 0 is the linear map h ↦ - x^{-1} h x^{-1}. That is, f'(x)(h) = - x^{-1} h x^{-1}.

Русский

В неконмутативном нормированном деленном кольце R производная отображения x ↦ x^{-1} в точке x ≠ 0 равна линейному отображению h ↦ − x^{-1} h x^{-1}.

LaTeX

$$$\\forall x \\neq 0,\\; f'(x)(h) = -\\,x^{-1} h\\, x^{-1}$$$

Lean4

/-- Non-commutative version of `fderiv_inv` -/
theorem fderiv_inv' {x : R} (hx : x ≠ 0) : fderiv 𝕜 Inv.inv x = -mulLeftRight 𝕜 R x⁻¹ x⁻¹ :=
  (hasFDerivAt_inv' hx).fderiv

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