contDiffAt_inv — Mathlib

English

In a complete normed algebra with a summable geometric series, the map x ↦ x^{-1} is C^n at each invertible x.

Русский

В полностью нормированном алгебраическом пространстве с суммируемым геометрическим рядом отображение x↦x^{-1} является C^n в каждой обратимой точке x.

LaTeX

$$$[HasSummableGeomSeries R]\\; (x\\in R^{\\times})\\; \\mathrm{ContDiffAt}_{\\mathbb{k}}\\ n \\mathrm{Ring.inverse}\\ x$$$

Lean4

@[fun_prop]
theorem contDiffAt_inv {x : 𝕜'} (hx : x ≠ 0) {n} : ContDiffAt 𝕜 n Inv.inv x := by
  simpa only [Ring.inverse_eq_inv'] using contDiffAt_ringInverse 𝕜 (Units.mk0 x hx)

Похожие утверждения