zpow — Mathlib

English

If f is analytic and nonzero on a set, then its integer powers f^n are analytic on that set.

Русский

Если f аналитична и не обращается в нуль на множестве, то f^n аналитично на этом множестве.

LaTeX

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

Lean4

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

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