analyticOnNhd_inverse — Mathlib

English

In a normed algebra A with HasSummableGeomSeries, the inversion map is analytic on a neighborhood of the set of units.

Русский

В нормированной алгебре A с суммируемой геометрической серией отображение инверсии аналитично в некоторой окрестности множества единиц.

LaTeX

$$AnalyticOnNhd 𝕜 Ring.inverse {x : A | IsUnit x}$$

Lean4

theorem analyticOnNhd_inverse {𝕜 : Type*} [NontriviallyNormedField 𝕜] {A : Type*} [NormedRing A] [NormedAlgebra 𝕜 A]
    [HasSummableGeomSeries A] : AnalyticOnNhd 𝕜 Ring.inverse {x : A | IsUnit x} := fun _ hx ↦
  analyticAt_inverse (IsUnit.unit hx)

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