Theorems · Theorem · complex analysis

meromorphicOrderAt_logDeriv_nonneg

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} [CompleteSpace 𝕜] {f : 𝕜 → 𝕜},
  MeromorphicAt f x → meromorphicOrderAt f x = 0 → 0 ≤ meromorphicOrderAt (logDeriv f) x

At points where a meromorphic function has order zero, the meromorphic order of the logarithmic derivative is nonnegative.

Defined in

Mathlib.Analysis.Meromorphic.Order

Cited by

0 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldCompleteSpace