English
For an invertible x in a normed division ring R, hasStrictFDerivAt Inv.inv equals -mulLeftRight 𝕜 R x^{-1} x^{-1}. This is a restatement of the Fréchet derivative of inversion.
Русский
Для инвертируемого x в нормированном деление кольце R, hasStrictFDerivAt Inv.inv равен -mulLeftRight 𝕜 R x^{-1} x^{-1}.
LaTeX
$$$\text{hasStrictFDerivAt_inv' } (x) : HasStrictFDerivAt Inv.inv (-mulLeftRight 𝕜 R x^{-1} x^{-1}) x$$$
Lean4
/-- At an invertible element `x` of a normed division algebra `R`, the Fréchet derivative of the
inversion operation is the linear map `fun t ↦ - x⁻¹ * t * x⁻¹`. For a nicer formula in the
commutative case, see `hasFDerivAt_inv`. -/
@[fun_prop]
theorem hasFDerivAt_inv' {x : R} (hx : x ≠ 0) : HasFDerivAt Inv.inv (-mulLeftRight 𝕜 R x⁻¹ x⁻¹) x := by
simpa using hasFDerivAt_ringInverse (Units.mk0 _ hx)
