English
Let E be an extension of F. If the top intermediate field of F-E is finitely generated as an F-algebra and E is algebraic over F, then E is finite-dimensional as a vector space over F.
Русский
Пусть E — расширение поля F. Если верхний промежуточный поле в цепочке F ⊆ E порождается порождением конечного множества элементов и E является алгебраическим над F, то E конечномерно над F.
LaTeX
$$$\text{If } E/F \text{ is algebraic and } \top_{F,E} \text{ is finitely generated as an } F\text{-algebra, then } [E:F] < \infty.$$$
Lean4
theorem finite_of_fg_of_isAlgebraic (h : IntermediateField.FG (⊤ : IntermediateField F E)) [Algebra.IsAlgebraic F E] :
Module.Finite F E := by
obtain ⟨s, hs⟩ := h
have : Algebra.FiniteType F E := by
use s
rw [← IntermediateField.adjoin_algebraic_toSubalgebra (fun x hx ↦ Algebra.IsAlgebraic.isAlgebraic x)]
simpa [← IntermediateField.toSubalgebra_inj] using hs
exact Algebra.IsIntegral.finite
