English
For a finite separable extension, there exists a primitive element α that generates E over F, hence E has a power basis F ⟮α⟯ = E.
Русский
Для конечного разделяемого расширения существует примитивный элемент α, порождающий E над F, следовательно E имеет степенной базис.
LaTeX
$$$\exists \alpha\in E,\ F\langle \alpha\rangle = E$$$
Lean4
theorem exists_primitive_element_of_finite_intermediateField [Finite (IntermediateField F E)]
(K : IntermediateField F E) : ∃ α : E, F⟮α⟯ = K :=
by
haveI := FiniteDimensional.of_finite_intermediateField F E
rcases finite_or_infinite F with (_ | _)
· obtain ⟨α, h⟩ := exists_primitive_element_of_finite_bot F K
exact ⟨α, by simpa only [lift_adjoin_simple, lift_top] using congr_arg lift h⟩
· apply induction_on_adjoin (fun K ↦ ∃ α : E, F⟮α⟯ = K) ⟨0, adjoin_zero⟩
rintro K β ⟨α, rfl⟩
simp_rw [adjoin_simple_adjoin_simple, eq_comm]
exact primitive_element_inf_aux_of_finite_intermediateField F α β
