pow — Mathlib

English

If f is meromorphic at x, then f^n is meromorphic at x for any natural n.

Русский

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

LaTeX

$$$MeromorphicAt f x \\to MeromorphicAt (f^n) x$$$

Lean4

@[fun_prop]
theorem pow {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (n : ℕ) : MeromorphicAt (f ^ n) x := by
  induction n with
  | zero => simpa only [pow_zero] using MeromorphicAt.const 1 x
  | succ m hm => simpa only [pow_succ] using hm.mul hf

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