of_exists_primitive_element — Mathlib

English

If E/F is a finite separable extension, there exists α ∈ E such that F⟮α⟯ = ⊤ (i.e., E is generated by a single element).

Русский

Для конечного разделяемого расширения существует α ∈ E such that F⟮α⟯ = ⊤.

LaTeX

$$$\exists \alpha\in E,\ F\langle \alpha\rangle = \top$$$

Lean4

theorem of_exists_primitive_element [Algebra.IsAlgebraic F E] (h : ∃ α : E, F⟮α⟯ = ⊤) : FiniteDimensional F E :=
  by
  obtain ⟨α, hprim⟩ := h
  have hfin := adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral (R := F) α)
  rw [hprim] at hfin
  exact topEquiv.toLinearEquiv.finiteDimensional

Похожие утверждения