functionField_iff

theorem functionField_iff : ∀ (Fq F : Type) [inst : Field Fq] [inst_1 : Field F] (Fqt : Type u_1) [inst_2 : Field Fqt] [inst_3 : Algebra (Polynomial Fq) Fqt] [inst_4 : IsFractionRing (Polynomial Fq) Fqt] [inst_5 : Algebra (RatFunc Fq) F] [inst_6 : Algebra Fqt F] [inst_7 : Algebra (Polynomial Fq) F] [inst_8 : IsScalarTower (Polynomial Fq) Fqt F] [inst_9 : IsScalarTower (Polynomial Fq) (RatFunc Fq) F], FunctionField Fq F ↔ FiniteDimensional Fqt F

The theorem `functionField_iff` states that a field `F` is a function field over another field `Fq` if and only if `F` is a finite extension of `Fq(t)`, where `t` is an indeterminate over `Fq`. Here, `Fq(t)` refers to the field of rational functions in one variable over `Fq`, and a finite extension means that `F` is a finite-dimensional vector space over `Fq(t)`. This is generalizing the idea of a function field in the case of algebraic geometry where `Fq(t)` is the field of rational functions on an algebraic curve.

More concisely: A field \(F\) is a function field over another field \(Fq\) if and only if \(F\) is a finite-dimensional vector space over \(Fq(t)\), where \(Fq(t)\) is the field of rational functions in one variable over \(Fq\).