English
Let x ↦ x^{-1} be the inversion map on a normed division ring with nontrivial norm. Then the map is differentiable at every nonzero x, and its Fréchet derivative at x is the linear map h ↦ - x^{-1} h x^{-1}. In particular, x ↦ x^{-1} is differentiable on {x ≠ 0}.
Русский
Пусть x ↦ x^{-1} — обращение в нормированном делении кольца; она дифференцируема во всех x ≠ 0, а её производная в точке x имеет вид h ↦ − x^{-1} h x^{-1}. Следовательно, обращение дифференцируемо на области {x ≠ 0}.
LaTeX
$$$\\forall x \\neq 0,\\quad D\\bigl(x \\mapsto x^{-1}\\bigr)_x(h) = -\\,x^{-1} h\\, x^{-1}$$$
Lean4
@[fun_prop]
theorem differentiableOn_inv : DifferentiableOn 𝕜 (fun x : R => x⁻¹) {x | x ≠ 0} := fun _x hx =>
differentiableWithinAt_inv hx _
