analyticAt_inv — Mathlib

English

In a normed algebra with HasSummableGeomSeries, the map z ↦ z^{-1} is analytic at any unit z.

Русский

В нормированной алгебре с суммируемой геометрической серией отображение z ↦ z^{-1} аналитично в любой единице z.

LaTeX

$$AnalyticAt 𝕜 Ring.inverse z$$

Lean4

/-- If `𝕝` is a normed field extension of `𝕜`, then the inverse map `𝕝 → 𝕝` is `𝕜`-analytic
away from 0. -/
@[fun_prop]
theorem analyticAt_inv {z : 𝕝} (hz : z ≠ 0) : AnalyticAt 𝕜 Inv.inv z :=
  by
  convert analyticAt_inverse (𝕜 := 𝕜) (Units.mk0 _ hz)
  exact Ring.inverse_eq_inv'.symm

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