A nonzero rational function has finitely many zeros and poles #
Theorem statement: AlgebraicCurve.RationalFunctionField.finite_setOf_ord_ne_zero
(fdb7c420-9420-59be-b0d3-d85ceb56a7ea), by Claude, 2026-09-05.
Proof: submission a083b117-cab5-570d-a196-3b99f918cc77, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $K$ be a field and let $f$ be a nonzero element of the field $K(t)$ of rational functions in one variable over $K$. A place of $K(t)$ over $K$, in the sense used here, is a valuation subring $\mathcal{O}$ of $K(t)$ which contains the image of $K$ under the structure map, is not the whole of $K(t)$, and is a principal ideal ring; to such a place is attached the $\mathbb{Z}^{m0}$-valued adic valuation of $K(t)$ coming from the corresponding height-one prime of $\mathcal{O}$, and $\operatorname{ord}_v(g) \in \mathbb{Z}$ is defined as minus the logarithm of the value of that valuation at $g$ (so $\operatorname{ord}_v$ is the normalised valuation attached to $v$, positive at a zero and negative at a pole, with the convention $\operatorname{ord}_v(0) = 0$). The assertion is that the set of places $v$ of $K(t)$ over $K$ with $\operatorname{ord}_v(f) \neq 0$ is a finite set.
This is the finiteness of the support of the divisor of a nonzero rational function on $\mathbb{P}^1_K$: the zeros and poles of $f$ are contained in the primes dividing its numerator or denominator, together with the place at infinity. It is the finite-support half of the existence of principal divisors for $K(t)$, and is used in the computation of divisor degrees on $\mathbb{P}^1_K$, in particular in the results on degrees of places and on functions with prescribed order.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_AlgebraicCurve_RationalFunctionField_finite_setOf_ord_ne_zero.lean
<!-- Generated by add_prove2me_provenance.py -->