English
The statement that an algebraic extension E/F has a primitive element is equivalent to the finiteness of the set of intermediate fields between E and F.
Русский
Существование примитивного элемента эквивалентно конечности множества промежуточных полей между E и F.
LaTeX
$$$(\text{Algebra.IsAlgebraic } F E \wedge \exists \alpha, F\langle \alpha\rangle = \top) \iff Finite(\text{IntermediateField } F E)$$$
Lean4
/-- **Steinitz theorem**: an algebraic extension `E` of `F` has a
primitive element (i.e. there is an `α ∈ E` such that `F⟮α⟯ = (⊤ : Subalgebra F E)`)
if and only if there exist only finitely many intermediate fields between `E` and `F`. -/
@[stacks 030N "Equivalence of (1) & (2)"]
theorem exists_primitive_element_iff_finite_intermediateField :
(Algebra.IsAlgebraic F E ∧ ∃ α : E, F⟮α⟯ = ⊤) ↔ Finite (IntermediateField F E) :=
⟨fun ⟨_, h⟩ ↦ finite_intermediateField_of_exists_primitive_element F E h, fun _ ↦
⟨isAlgebraic_of_finite_intermediateField F E, exists_primitive_element_of_finite_intermediateField F E _⟩⟩
