Finitely generated fraction fields

A fraction field of a finitely generated domain is finitely generated as a field extension. The conclusion uses IntermediateField.FG, rather than finite type as an algebra: a transcendental fraction field is generally not finitely generated as an algebra over its ground field.

theorem AlgebraicAnalysis.FunctionField.top_fg_of_finiteType_fractionRing (k : Type u) (A : Type v) (K : Type w) [Field k] [CommRing A] [Algebra k A] [Field K] [Algebra A K] [IsFractionRing A K] [Algebra k K] [IsScalarTower k A K] [Algebra.FiniteType k A] : ⊤.FG

The fraction field of a finitely generated domain is a finitely generated field extension of the ground field.