Theorems · Theorem · complex analysis

Function.FactorizedRational.divisor

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {D : Function.locallyFinsuppWithin U ℤ},
  D.support.Finite → MeromorphicOn.divisor (∏ᶠ (u : 𝕜), (fun x => x - u) ^ D u) U = D

If D is a divisor, then the divisor of the factorized rational function equals D.

Defined in

Mathlib.Analysis.Meromorphic.FactorizedRational

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedField