English
For an invertible element x in a normed ring R, the map Ring.inverse is strictly Fréchet differentiable at x with derivative the bilinear map t ↦ - x^{-1} t x^{-1}. In the unit case, this is expressed as the derivative of Inv.inv is -mulLeftRight 𝕜 R x^{-1} x^{-1}.
Русский
Для обратимого элемента x в нормированном кольце R отображение обратной операции имеет строгую Ферше-дифференцируемость в x, производная задаётся как тождество t ↦ - x^{-1} t x^{-1}. В случае единиц это записано как производная Inv.inv = -mulLeftRight 𝕜 R x^{-1} x^{-1}.
LaTeX
$$$\text{Let } x \in R^{\times}.\; D_x\,\text{Ring.inverse} = - (x^{-1} \cdot (·) \cdot x^{-1}).$$$
Lean4
theorem fderivWithin_finset_prod [DecidableEq ι] {x : E} (hxs : UniqueDiffWithinAt 𝕜 s x)
(hg : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (g i) s x) :
fderivWithin 𝕜 (∏ i ∈ u, g i ·) s x = ∑ i ∈ u, (∏ j ∈ u.erase i, (g j x)) • fderivWithin 𝕜 (g i) s x :=
(HasFDerivWithinAt.finset_prod fun i hi ↦ (hg i hi).hasFDerivWithinAt).fderivWithin hxs
