English
Let f be analytic on a neighborhood s and assume f never vanishes on s. Then for any integer n, the function x ↦ f(x)^n is analytic on s.
Русский
Пусть f аналитична на окрестности s и на s нигде не обращается в нуль. Тогда функция x ↦ f(x)^n аналитична на s для любого целого n.
LaTeX
$$$\\text{If } f:E\\to\\mathfrak{L} \\\\text{ is AnalyticOn 𝕜 on } s \\text{ and } \\forall z\\in s: f(z) \\neq 0, \\text{ then } (f)^n: E\\to \\mathfrak{L} \\text{ is AnalyticOn 𝕜 on } s.$$$
Lean4
/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
-/
theorem fun_zpow {f : E → 𝕝} {s : Set E} {n : ℤ} (h₁f : AnalyticOnNhd 𝕜 f s) (h₂f : ∀ z ∈ s, f z ≠ 0) :
AnalyticOnNhd 𝕜 (fun x ↦ f x ^ n) s := fun z hz ↦ (h₁f z hz).zpow (h₂f z hz)
