Theorems · Theorem · complex analysis

Function.FactorizedRational.mulSupport

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] (d : 𝕜 → ℤ),
  (Function.mulSupport fun u => (fun x => x - u) ^ d u) = Function.support d

Helper Lemma: Identify the support of d as the mulsupport of the product defining the factorized rational function.

Defined in

Mathlib.Analysis.Meromorphic.FactorizedRational

Cited by

6 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedField