ringOfIntegers — Mathlib

English

The ring of integers of a function field is the integral closure of F_q[X] in F.

Русский

Целочисленный кольцо функции — это целочисленное замыкание F_q[X] в F.

LaTeX

$$$\\text{ringOfIntegers}(F_q,F) = \\text{integralClosure}(F_q[X],F)$$$

Lean4

/-- The function field analogue of `NumberField.ringOfIntegers`:
`FunctionField.ringOfIntegers Fq Fqt F` is the integral closure of `Fq[t]` in `F`.

We don't actually assume `F` is a function field over `Fq` in the definition,
only when proving its properties.
-/
def ringOfIntegers [Algebra Fq[X] F] :=
  integralClosure Fq[X] F

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