fun_pow

Mathlib.Analysis.Meromorphic.Basic

URI: https://scilib.ai/kg/mathlib#MeromorphicAt.fun_pow

English

Let f be meromorphic at x. Then for any n ∈ ℕ, f^n is meromorphic at x.

Русский

Пусть f мероморфна в x. Тогда для любого n∈ℕ f^n мероморфна в x.

LaTeX

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

Lean4

@[fun_prop]
theorem fun_pow {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (n : ℕ) : MeromorphicAt (fun z ↦ (f z) ^ n) x :=
  hf.pow n

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru