Theorems · Theorem · complex analysis

Complex.CanonicalDecomp.divisor_eq_divisor

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R : ℝ} {f g : ℂ → E} {x : ℂ},
  Complex.CanonicalDecomp f g R →
    0 < R → (MeromorphicOn.divisor g (Metric.closedBall 0 R)) x = (MeromorphicOn.divisor f (Metric.sphere 0 R)) x

Given a canonical decomposition CanonicalDecomp f g R, the function associated with the divisor of g equals the function associated with the divisor of f, seen as a meromorphic function on the sphere.

Defined in

Mathlib.Analysis.Complex.CanonicalDecomposition

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace