English
If F is infinite and α, β ∈ E are separable over F, then there exists γ ∈ E with F⟮α, β⟯ = F⟮γ⟯; this is the core step in primitive element theorem for two generators.
Русский
Если F бесконечно, а α, β ∈ E над F раздельны, то существует γ ∈ E с F⟮α, β⟯ = F⟮γ⟯; это ключевой шаг теоремы о примитивном элементе для двух порождающих элементов.
LaTeX
$$$\exists \gamma\in E,\ F\langle \alpha, \beta\rangle = F\langle \gamma\rangle$$$
Lean4
/-- Alternative phrasing of primitive element theorem:
a finite separable field extension has a basis `1, α, α^2, ..., α^n`.
See also `exists_primitive_element`. -/
noncomputable def powerBasisOfFiniteOfSeparable : PowerBasis F E :=
let α := (exists_primitive_element F E).choose
let pb := adjoin.powerBasis (Algebra.IsSeparable.isIntegral F α)
have e : F⟮α⟯ = ⊤ := (exists_primitive_element F E).choose_spec
pb.map ((IntermediateField.equivOfEq e).trans IntermediateField.topEquiv)
