English
For a subset s of a normed division ring R, the noncommutative formula for the derivative of the inverse holds inside s: if x ≠ 0 and we consider f(x) = x^{-1}, then f'(x) is the map h ↦ - x^{-1} h x^{-1} provided the point lies in s with the usual differentiability inside s.
Русский
Для подмножества s в нормированном деленном кольце R формула производной обращения x ↦ x^{-1} сохраняется внутри s: при наличии x ≠ 0 и допустимости внутри s, производная равна h ↦ - x^{-1} h x^{-1}.
LaTeX
$$$\\forall x \\in s,\\; x \\neq 0 \\Rightarrow D\\bigl(x \\mapsto x^{-1}\\bigr)_x(h) = -x^{-1} h x^{-1}$$$
Lean4
/-- Non-commutative version of `fderivWithin_inv` -/
theorem fderivWithin_inv' {s : Set R} {x : R} (hx : x ≠ 0) (hxs : UniqueDiffWithinAt 𝕜 s x) :
fderivWithin 𝕜 (fun x => x⁻¹) s x = -mulLeftRight 𝕜 R x⁻¹ x⁻¹ :=
by
rw [DifferentiableAt.fderivWithin (differentiableAt_inv hx) hxs]
exact fderiv_inv' hx
