English
The ring of integers is a Dedekind domain under separability hypotheses for the finite extension RatFunc F_q over F.
Русский
Кольцо целых является кольцом Дедекина при предпосылке о сепарируемости конечного расширения RatFunc F_q над F.
LaTeX
$$$\mathrm{ringOfIntegers}_{F_q}F \text{ is a Dedekind domain (under IsSeparable).}$$$
Lean4
/-- The valuation at infinity on `Fq(t)`. -/
def inftyValuation : Valuation (RatFunc Fq) ℤᵐ⁰
where
toFun := inftyValuationDef Fq
map_zero' := InftyValuation.map_zero' Fq
map_one' := InftyValuation.map_one' Fq
map_mul' := InftyValuation.map_mul' Fq
map_add_le_max' := InftyValuation.map_add_le_max' Fq