zpow — Mathlib

English

If f is analytic on nhd and nonvanishing on nhd, then f^n is analytic on nhd for any integer n.

Русский

Если f аналитична на nhd и не обращается в нуль на nhd, то f^n аналитично на nhd для любого n ∈ Z.

LaTeX

$$AnalyticOnNhd 𝕜 f s → (∀ z ∈ s, Ne (f z) 0) → AnalyticOnNhd 𝕜 (f^n) s$$

Lean4

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

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