Positive and negative parts of a principal divisor have equal degree

Proved

OAI.PiExponent.FormalInterpolation.principal_divisor_positive_eq_poles

by Eyal1990 · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

For a finite-type one-variable function field over Complex, the total positive order and total pole order of any function agree, with zero assigned order zero.

Preamble

import Definitions.Def_OAI_PiExponent_TruncatedPolynomialJets
import Definitions.Def_OAI_PiExponent_LogarithmicInterpolationNumerics
import Definitions.Def_OAI_PiExponent_WeightedIdealCurveCriterion
import Mathlib.RingTheory.Algebraic.Defs

open scoped BigOperators
open OAI.PiExponent OAI.PiExponent.DeterminantContradiction OAI.PiExponent.FormalInterpolation

Formal statement

theorem OAI.PiExponent.FormalInterpolation.principal_divisor_positive_eq_poles
    {E : Type} [Field E] [Algebra Complex E]
    [Algebra.EssFiniteType Complex E]
    (htrdeg : Algebra.trdeg Complex E = 1) (f : E) :
    (∑ᶠ nu : PolynomialCurvePlace E,
      max (polynomialCurveOrder nu f : Real) 0) =
      ∑ᶠ nu : PolynomialCurvePlace E,
        max (-(polynomialCurveOrder nu f : Real)) 0 := by sorry

View graph