Constants have order of vanishing zero at every place #
Theorem statement: AlgebraicCurve.Place.ord_algebraMap (e9cbc30c-79d6-5e63-be12-ce80e24a3ecf),
by Claude, 2026-09-05.
Proof: submission 3e52d324-acb0-5f10-abfd-f730853be6f1, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $K$ and $F$ be fields with $F$ a $K$-algebra, and let $v$ be a place of $F$ over $K$ in the
sense of the structure AlgebraicCurve.Place: a
valuation subring v.toValuationSubring of $F$ which contains $\mathrm{algebraMap}_{K\to F}(a)$ for
every $a\in K$, which is not all of $F$, and which is a principal ideal ring. Attached to $v$ is the
valuation v.adicValuation on $F$ with values in $\mathbb{Z}^{m0}=\mathbb{Z}\cup\{0\}$ (the
multiplicative integers with a zero adjoined), namely the valuation of the height-one prime
v.heightOneSpectrum of the valuation ring, and the integer-valued order function
$v.\mathrm{ord}(f) = -\log\bigl(v.\mathrm{adicValuation}(f)\bigr)$, where WithZero.log sends the
adjoined zero to $0$. The assertion is that for every $c\in K$ one has
$v.\mathrm{ord}\bigl(\mathrm{algebraMap}_{K\to F}(c)\bigr)=0$; in particular the convention for
$c=0$ is included, the order of $0$ being $0$.
This is the standard fact that elements of the constant field are units at every place of the function field $F/K$, so that they contribute no divisor; it is the basic step showing that the divisor map kills $K^{\times}$. It is used pervasively throughout the development of divisors and the divisor class group, and in the estimates for functions on annuli that rely on it.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_AlgebraicCurve_Place_ord_algebraMap.lean
<!-- Generated by add_prove2me_provenance.py -->