divisor — Mathlib

English

If D is a finite divisor on U, then the divisor of the factorized rational function ∏ᶠ u (· − u)^{D(u)} on U equals D.

Русский

Если D — конечный делитель на U, тогда дивизор функции ∏ᶠ u (· − u)^{D(u)} на U равен D.

LaTeX

$$$\MeromorphicOn.divisor\bigl(\prod^{\mathrm{fin}}_{u} (\cdot - u)^{D(u)}\bigr) U = D$$$

Lean4

/-- If `D` is a divisor, then the divisor of the factorized rational function equals `D`.
-/
theorem divisor {U : Set 𝕜} {D : locallyFinsuppWithin U ℤ} (hD : D.support.Finite) :
    MeromorphicOn.divisor (∏ᶠ u, (· - u) ^ D u) U = D := by
  ext z
  by_cases hz : z ∈ U <;> simp [(meromorphicNFOn D U).meromorphicOn, hz, meromorphicOrderAt_eq D hD]

Похожие утверждения