English
Let f: E → 𝕝 be analytic on a neighborhood of a set s ⊆ E, and assume f(z) ≠ 0 for every z ∈ s. Then for every integer n, the function z ↦ f(z)^n is analytic on s.
Русский
Пусть f: E → 𝕝 аналитична в окрестности множества s ⊆ E, и для каждого z ∈ s имеет место f(z) ≠ 0. Тогда для любого целого n функция z ↦ f(z)^n аналитична на s.
LaTeX
$$$\mathit{AnalyticOnNhd}_{\mathfrak k}(f,s) \wedge \bigl( \forall z \in s, f(z) \neq 0 \bigr) \Rightarrow \forall n \in \mathbb Z,\ \mathit{AnalyticOnNhd}_{\mathfrak k}(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 : AnalyticOnNhd 𝕜 f s) (h₂f : ∀ z ∈ s, f z ≠ 0) :
AnalyticOnNhd 𝕜 (f ^ n) s :=
fun_zpow h₁f h₂f
