English
Differentiability of the inverse map is inherited under differentiable maps and units; the derivative is the standard -x^{-1} t x^{-1} form.
Русский
Дифференцируемость обратной операции сохраняется под дифференцируемыми отображениями и единицами; производная принимает стандартную форму -x^{-1} t x^{-1}.
LaTeX
$$$\text{DifferentiableAt } Inv.inv x = -x^{-1} (D x) x^{-1}$$$
Lean4
/-- At an invertible element `x` of a normed division algebra `R`, the inversion is strictly
differentiable, with derivative the linear map `fun t ↦ - x⁻¹ * t * x⁻¹`. For a nicer formula in
the commutative case, see `hasStrictFDerivAt_inv`. -/
theorem hasStrictFDerivAt_inv' {x : R} (hx : x ≠ 0) : HasStrictFDerivAt Inv.inv (-mulLeftRight 𝕜 R x⁻¹ x⁻¹) x := by
simpa using hasStrictFDerivAt_ringInverse (Units.mk0 _ hx)
