English
A function field over F_q is a field F that is a finite extension of the rational function field in one variable over F_q.
Русский
Функциональное поле над F_q — это поле F, являющееся конечным расширением поля рациональных дробей в одну переменную над F_q.
LaTeX
$$$\\text{FunctionField}(F_q,F) \\iff \\text{FiniteDimensional}_{\\operatorname{RatFunc}(F_q)} F$$$
Lean4
/-- `F` is a function field over the finite field `Fq` if it is a finite
extension of the field of rational functions in one variable over `Fq`.
Note that `F` can be a function field over multiple, non-isomorphic, `Fq`.
-/
abbrev FunctionField [Algebra (RatFunc Fq) F] : Prop :=
FiniteDimensional (RatFunc Fq) F
