English
If the set of intermediate fields between F and E is finite, then E is finite-dimensional over F.
Русский
Если набор промежуточных полей между F и E конечен, то E конечномерно над F.
LaTeX
$$$\text{Finite }(\text{IntermediateField } F E)\Rightarrow \dim_F E<\infty$$$
Lean4
theorem of_finite_intermediateField [Finite (IntermediateField F E)] : FiniteDimensional F E :=
by
let IF := { K : IntermediateField F E // ∃ x, K = F⟮x⟯ }
have := isAlgebraic_of_finite_intermediateField F E
haveI : ∀ K : IF, FiniteDimensional F K.1 := fun ⟨_, x, rfl⟩ ↦
adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral _)
have hfin := finiteDimensional_iSup_of_finite (t := fun K : IF ↦ K.1)
have htop : ⨆ K : IF, K.1 = ⊤ :=
le_top.antisymm fun x _ ↦ le_iSup (fun K : IF ↦ K.1) ⟨F⟮x⟯, x, rfl⟩ <| mem_adjoin_simple_self F x
rw [htop] at hfin
exact topEquiv.toLinearEquiv.finiteDimensional
