Theorems · Definition · complex analysis

MeromorphicOn.divisor

{𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → (𝕜 → E) → (U : Set 𝕜) → Function.locallyFinsuppWithin U ℤ

The divisor of a meromorphic function f, mapping a point z to the order of f at z, and to zero if the order is infinite.

Defined in

Mathlib.Analysis.Meromorphic.Divisor

Cited by

90 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace