inftyValuation — Mathlib

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

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