zpow — Mathlib

English

If f is meromorphic at x, then f^n is meromorphic at x for any integer n (positive, negative, or zero).

Русский

Если f мероморфна в x, то f^n мероморфна в x для любого целого n (положительного, отрицательного или нуля).

LaTeX

$$$MeromorphicAt f x \\to \\forall n \\in \\mathbb{Z}, MeromorphicAt (f^n) x$$$

Lean4

@[fun_prop]
theorem zpow {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (n : ℤ) : MeromorphicAt (f ^ n) x := by
  cases n with
  | ofNat m => simpa only [Int.ofNat_eq_coe, zpow_natCast] using hf.pow m
  | negSucc m => simpa only [zpow_negSucc, inv_iff] using hf.pow (m + 1)

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