zpow — Mathlib

English

If f is analytic at z and f(z) ≠ 0, then f(z)^n is analytic at z for any integer n.

Русский

Если f аналитична в z и f(z) ≠ 0, то f(z)^n аналитично в z для любого целого n.

LaTeX

$$AnalyticAt 𝕜 f z → Ne (f z) 0 → AnalyticAt 𝕜 (f(z)^n) z$$

Lean4

/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
-/
theorem zpow {f : E → 𝕝} {z : E} {s : Set E} {n : ℤ} (h₁f : AnalyticWithinAt 𝕜 f s z) (h₂f : f z ≠ 0) :
    AnalyticWithinAt 𝕜 (f ^ n) s z :=
  fun_zpow h₁f h₂f

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