Theorems · Definition · complex analysis

meromorphicTrailingCoeffAt

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

If f is meromorphic of finite order at a point x, the trailing coefficient is defined as the (unique!) value g x for a presentation of f in the form (z - x) ^ order • g z with g analytic at x. In all other cases, the trailing coefficient is defined to be zero.

Defined in

Mathlib.Analysis.Meromorphic.TrailingCoefficient

Cited by

61 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace