Theorems · Theorem · complex analysis

Function.FactorizedRational.meromorphicOrderAt_eq

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {z : 𝕜} (d : 𝕜 → ℤ),
  Function.HasFiniteSupport d → meromorphicOrderAt (∏ᶠ (u : 𝕜), (fun x => x - u) ^ d u) z = ↑(d z)

The order of the factorized rational function (∏ᶠ u, fun z ↦ (z - u) ^ d u) at z equals d z.

Defined in

Mathlib.Analysis.Meromorphic.FactorizedRational

Cited by

3 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedField