fun_div

Mathlib.Analysis.Meromorphic.Basic

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

← MathLib Explorer

English

If f and g are meromorphic at x, then f/g is meromorphic at x.

Русский

Если f и g мероморфны в x, то f/g мероморфна в x.

LaTeX

$$$MeromorphicAt f x \\to MeromorphicAt g x \\to MeromorphicAt (instHDiv.hDiv f g) x$$$

Lean4

@[fun_prop]
theorem fun_div {f g : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
    MeromorphicAt (fun z ↦ f z / g z) x :=
  hf.div hg

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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