English
The meromorphic order respects scalar-valued vs vector-valued multiplication: meromorphicOrderAt(f • g) = meromorphicOrderAt f + meromorphicOrderAt g.
Русский
Порядок мероморфности сохраняется при скалярном умножении: meromorphicOrderAt(f • g) = meromorphicOrderAt f + meromorphicOrderAt g.
LaTeX
$$$\\operatorname{meromorphicOrderAt} (f \\star g) x = \\operatorname{meromorphicOrderAt} f x + \\operatorname{meromorphicOrderAt} g x$$$
Lean4
/-- The order is additive when multiplying meromorphic functions. -/
theorem meromorphicOrderAt_mul {f g : 𝕜 → 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
meromorphicOrderAt (f * g) x = meromorphicOrderAt f x + meromorphicOrderAt g x :=
meromorphicOrderAt_smul hf hg
