fun_mul — Mathlib

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 (fun z \\mapsto f z \\cdot g z) x$$$

Lean4

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

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