v-adic valuation as exp of minus the multiplicity of v #
Theorem statement: IsDedekindDomain.HeightOneSpectrum.valuation_eq_exp_neg_count
(bd555933-1cd7-5e0f-bba0-cf3d5fefac90), by Claude, 2026-09-05.
Proof: submission 5579bf6c-bb3f-58ad-83a1-88349d199c9d, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $R$ be a commutative ring which is a Dedekind domain, let $K$ be a field equipped with an
$R$-algebra structure making it a fraction field of $R$, let $v$ be a point of the height-one
spectrum of $R$ (a nonzero prime ideal of height one), and let $x \in K$ with $x \neq 0$. The
assertion is that the multiplicative $v$-adic valuation $v(x)$ of $x$ on $K$, in the sense of
Mathlib's IsDedekindDomain.HeightOneSpectrum.valuation, taking values in $\mathbb{Z}$ with a zero
adjoined, equals $\exp(-n)$, where $n =$ FractionalIdeal.count K v (FractionalIdeal.spanSingleton R⁰ x) is the exponent of $v$ in the factorisation into powers of height-one primes of the principal
fractional ideal $xR \subseteq K$ generated by $x$ (here $R⁰$ denotes the monoid of
non-zero-divisors of $R$, with respect to which the fractional ideals are formed), and $\exp$ is the
embedding of the additive group $\mathbb{Z}$ into the multiplicative monoid $\mathbb{Z}$-with-zero.
Thus the two Mathlib descriptions of the order of $x$ at $v$ — through the valuation and through the
ideal factorisation — agree, with the normalisation in which a uniformiser has valuation $\exp(-1)$.
This is the classical identification of the exponential valuation $v_{\mathfrak p}$ on the fraction field of a Dedekind domain with the multiplicity of $\mathfrak p$ in the principal ideal $(x)$, i.e. $(x) = \prod_{\mathfrak p} \mathfrak p^{v_{\mathfrak p}(x)}$. It serves as the bridge allowing orders of zeros and poles to be computed from ideal factorisations; it is used in the treatment of valuations of functions on Weierstrass curves and in an estimate for automorphic forms.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_IsDedekindDomain_HeightOneSpectrum_valuation_eq_exp_neg_count.lean
<!-- Generated by add_prove2me_provenance.py -->