Theorems · Theorem · complex analysis

Complex.divisor_canonicalFactor

∀ {R : ℝ} {w : ℂ},
  w ∈ Metric.ball 0 R →
    MeromorphicOn.divisor (Complex.canonicalFactor R w) (Metric.ball 0 R) =
      -Function.locallyFinsuppWithin.restrict (Function.locallyFinsuppWithin.single w 1) ⋯

The divisor of CanonicalFactor R w is -w. In other words, the divisor function takes the value -1 at w and is zero elsewhere.

Defined in

Mathlib.Analysis.Complex.CanonicalDecomposition

Cited by

0 results in Mathlib

Foundations

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