English
If f is analytic within s and f(x) ≠ 0 for all x in s, then (f x)^{-1} is analytic within s.
Русский
Если f аналитична внутри s и f(x) не равно нулю на s, то (f(x))^{-1} аналитично внутри s.
LaTeX
$$AnalyticWithinAt 𝕜 f s x → (∀ x ∈ s, f x ≠ 0) → AnalyticWithinAt 𝕜 (f x)^{-1} s x$$
Lean4
/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
-/
theorem fun_zpow {f : E → 𝕝} {z : E} {s : Set E} {n : ℤ} (h₁f : AnalyticWithinAt 𝕜 f s z) (h₂f : f z ≠ 0) :
AnalyticWithinAt 𝕜 (fun x ↦ f x ^ n) s z := by
by_cases hn : 0 ≤ n
· exact zpow_nonneg h₁f hn
· rw [(Int.eq_neg_comm.mp rfl : n = -(-n))]
conv => arg 2; intro x; rw [zpow_neg]
exact (h₁f.zpow_nonneg (by linarith)).inv (zpow_ne_zero (-n) h₂f)
