English
If E is a finite extension of F (finite-dimensional over F), there exists an element α in E such that the subalgebra generated by α over F is the whole field E.
Русский
Если расширение E/F конечносеместровое, то существует элемент α ∈ E такой, что F⟮α⟯ = ⊤ (то есть все E генерируется α над F).
LaTeX
$$$\exists \alpha\in E,\ F\langle \alpha\rangle = \top$$$
Lean4
/-- **Primitive element theorem** assuming E is finite. -/
@[stacks 09HY "second part"]
theorem exists_primitive_element_of_finite_top [Finite E] : ∃ α : E, F⟮α⟯ = ⊤ :=
by
obtain ⟨α, hα⟩ := @IsCyclic.exists_generator Eˣ _ _
use α
rw [eq_top_iff]
rintro x -
by_cases hx : x = 0
· rw [hx]
exact F⟮α.val⟯.zero_mem
· obtain ⟨n, hn⟩ := Set.mem_range.mp (hα (Units.mk0 x hx))
rw [show x = α ^ n by norm_cast; rw [hn, Units.val_mk0]]
exact zpow_mem (mem_adjoin_simple_self F (E := E) ↑α) n
