Theorems · Theorem · complex analysis

Function.FactorizedRational.meromorphicTrailingCoeffAt_factorizedRational

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

Compute the trailing coefficient of the factorized rational function associated with d : 𝕜 → ℤ.

Defined in

Mathlib.Analysis.Meromorphic.FactorizedRational

Cited by

3 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedField