mul

Mathlib.Analysis.Meromorphic.Basic

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

English

Let f, g: 𝕜 → 𝕜 be meromorphic at x. Then f · g is meromorphic at x.

Русский

Пусть f и g: 𝕜 → 𝕜 мероморфны в x. Тогда f(z) · g(z) мероморфна в x.

LaTeX

$$$MeromorphicAt f x \\to MeromorphicAt g x \\to MeromorphicAt (instHMul.hMul f g) x$$$

Lean4

@[fun_prop]
theorem mul {f g : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) : MeromorphicAt (f * g) x :=
  hf.smul hg

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

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

Разделы

Аффилиация

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