inftyValuationDef — Mathlib

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

Похожие утверждения