English
If f1, f2 are meromorphic on U and certain finiteness conditions hold for orders, then the divisor of their product equals the sum of their divisors.
Русский
Если f1, f2 мероморфны на U и выполнены условия конечности порядков, то делитель произведения равен сумме делителей.
LaTeX
$$$\text{MeromorphicOn}(f_1, U) \land \text{MeromorphicOn}(f_2, U) \land \Big(\forall z\in U, meromorphicOrderAt(f_1,z) \neq \top \land meromorphicOrderAt(f_2,z) \neq \top\Big) \Rightarrow \text{divisor}(f_1 f_2, U) = \text{divisor}(f_1, U) + \text{divisor}(f_2, U)$$$
Lean4
/-- If orders are finite, the divisor of the product of two meromorphic functions is the sum of the
divisors.
See `MeromorphicOn.exists_order_ne_top_iff_forall` and
`MeromorphicOn.order_ne_top_of_isPreconnected` for two convenient criteria to guarantee conditions
`h₂f₁` and `h₂f₂`.
-/
theorem divisor_mul {f₁ f₂ : 𝕜 → 𝕜} (h₁f₁ : MeromorphicOn f₁ U) (h₁f₂ : MeromorphicOn f₂ U)
(h₂f₁ : ∀ z ∈ U, meromorphicOrderAt f₁ z ≠ ⊤) (h₂f₂ : ∀ z ∈ U, meromorphicOrderAt f₂ z ≠ ⊤) :
divisor (f₁ * f₂) U = divisor f₁ U + divisor f₂ U :=
divisor_smul h₁f₁ h₁f₂ h₂f₁ h₂f₂
