Theorems · Theorem · complex analysis

MeromorphicOn.divisor_mul

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {f₁ f₂ : 𝕜 → 𝕜},
  MeromorphicOn f₁ U →
    MeromorphicOn f₂ U →
      (∀ z ∈ U, meromorphicOrderAt f₁ z ≠ ⊤) →
        (∀ z ∈ U, meromorphicOrderAt f₂ z ≠ ⊤) →
          MeromorphicOn.divisor (f₁ * f₂) U = MeromorphicOn.divisor f₁ U + MeromorphicOn.divisor f₂ U

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₂.

Defined in

Mathlib.Analysis.Meromorphic.Divisor

Cited by

3 results in Mathlib

Foundations

Depth 209 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedField