Theorems · Theorem · complex analysis

Function.FactorizedRational.extractFactor

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

Helper Lemma for Computations: Extract one factor out of a factorized rational function.

Defined in

Mathlib.Analysis.Meromorphic.FactorizedRational

Cited by

2 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedField