analyticOnNhd_inv — Mathlib

English

If 𝕝 is a normed field extension of 𝕜 and the algebra structure is present, then inv is analytic on a neighborhood of the units.

Русский

Если 𝕝 является нормированным полем-расширением 𝕜 и имеется структура алгебры, то отображение inv аналитично на окрестности единиц.

LaTeX

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

Lean4

/-- `x⁻¹` is analytic away from zero -/
theorem analyticOnNhd_inv : AnalyticOnNhd 𝕜 (fun z ↦ z⁻¹) {z : 𝕝 | z ≠ 0} := by intro z m; exact analyticAt_inv m

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