PolynomialCurvePlace order support is finite given HasPrincipalDivisors

Assume $E/\mathbb{C}$ admits principal divisors in the sense of AlgebraicCurve.HasPrincipalDivisors: for every nonzero $f\in E$ the function $v\mapsto v.\mathrm{ord}(f)$ on AlgebraicCurve.Place places is the evaluation of a finitely supported divisor.

Then, among the normalized discrete places of type PolynomialCurvePlace (integer-valued additive valuations trivial on $\mathbb{C}^\times$ and surjective onto $\mathbb{Z}$), only finitely many $\nu$ satisfy $\mathrm{ord}_\nu(f)\neq 0$.

This is the comparison between the FormalInterpolation place type and the AlgebraicCurve place type: once principal divisors exist for the latter, the nonzero-order locus for the former is finite. The zero function is assigned order zero at every place by the untop₀ convention, so its support is empty.