fun_zpow — Mathlib

English

If a function f is meromorphic at a point x, then for every integer n, the function z ↦ (f(z))^n is meromorphic at x.

Русский

Если функция f мероморфна в точке x, то для каждого целого числа n функция z ↦ (f(z))^n мероморфна в x.

LaTeX

$$$MeromorphicAt f x \rightarrow \forall n \in \mathbb{Z},\ MeromorphicAt (fun z \mapsto (f z)^n) x$$$

Lean4

@[fun_prop]
theorem fun_zpow {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (n : ℤ) : MeromorphicAt (fun z ↦ (f z) ^ n) x :=
  hf.zpow n

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