hasStrictFDerivAt_ringInverse — Mathlib

English

For an invertible x in a normed ring R, hasStrictFDerivAt Ring.inverse at x holds with derivative -mulLeftRight 𝕜 R x^{-1} x^{-1}. This matches the general inverse derivative in noncommutative setting.

Русский

Для обратимого x в нормированном кольце R имеет место строгая производная Ring.inverse в x с производной -mulLeftRight 𝕜 R x^{-1} x^{-1}.

LaTeX

$$$\text{HasStrictFDerivAt Ring.inverse } (-\mathrm{mulLeftRight} 𝕜 R x^{-1} x^{-1}) x.$$$

Lean4

theorem hasStrictFDerivAt_ringInverse (x : Rˣ) : HasStrictFDerivAt Ring.inverse (-mulLeftRight 𝕜 R ↑x⁻¹ ↑x⁻¹) x :=
  by
  convert (analyticAt_inverse (𝕜 := 𝕜) x).hasStrictFDerivAt
  exact (fderiv_inverse x).symm

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