English
There exists a nonarchimedean valuation on the function field that is the valuation at infinity.
Русский
Существует неархимова валюация на поле функций, которая является валиацией на бесконечности.
LaTeX
$$$\text{There exists a nonarchimedean valuation } v \text{ on } \mathrm{RatFunc}_{F_q} \text{ with value group } \mathrm{WithZero}(\mathrm{Multiplicative}(\mathbb{Z})).$$$
Lean4
/-- The valuation at infinity is the nonarchimedean valuation on `Fq(t)` with uniformizer `1/t`.
Explicitly, if `f/g ∈ Fq(t)` is a nonzero quotient of polynomials, its valuation at infinity is
`exp (degree(f) - degree(g))`. -/
def inftyValuationDef (r : RatFunc Fq) : ℤᵐ⁰ :=
if r = 0 then 0 else exp r.intDegree