Theorems · Definition · complex analysis

meromorphicOrderAt

{𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} → [inst_1 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → (𝕜 → E) → 𝕜 → WithTop ℤ

The order of a meromorphic function f at z₀, as an element of ℤ ∪ {∞}. The order is defined to be ∞ if f is identically 0 on a neighbourhood of z₀, and otherwise the unique n such that f can locally be written as f z = (z - z₀) ^ n • g z, where g is analytic and does not vanish at z₀. See MeromorphicAt.meromorphicOrderAt_eq_top_iff and MeromorphicAt.meromorphicOrderAt_eq_int_iff for these equivalences. If the function is not meromorphic at x, we use the junk value 0.

Defined in

Mathlib.Analysis.Meromorphic.Order

Cited by

180 results in Mathlib

Foundations

Depth 195 from the axioms, rests on 5,362 definitions · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace