Primitive Element Theorem #
In this file we prove the primitive element theorem.
Main results #
exists_primitive_element
: a finite separable extensionE / F
has a primitive element, i.e. there is anα : E
such thatF⟮α⟯ = (⊤ : subalgebra F E)
.
Implementation notes #
In declaration names, primitive_element
abbreviates adjoin_simple_eq_top
:
it stands for the statement F⟮α⟯ = (⊤ : subalgebra F E)
. We did not add an extra
declaration is_primitive_element F α := F⟮α⟯ = (⊤ : subalgebra F E)
because this
requires more unfolding without much obvious benefit.
Tags #
primitive element, separable field extension, separable extension, intermediate field, adjoin, exists_adjoin_simple_eq_top
Primitive element theorem for finite fields #
Primitive element theorem for infinite fields #
Primitive element theorem: a finite separable field extension E
of F
has a
primitive element, i.e. there is an α ∈ E
such that F⟮α⟯ = (⊤ : subalgebra F E)
.
Alternative phrasing of primitive element theorem:
a finite separable field extension has a basis 1, α, α^2, ..., α^n
.
See also exists_primitive_element
.
Equations
- field.power_basis_of_finite_of_separable F E = let α : E := _.some, pb : power_basis F ↥F⟮α⟯ := intermediate_field.adjoin.power_basis _ in have e : F⟮α⟯ = ⊤, from _, pb.map ((intermediate_field.equiv_of_eq e).trans intermediate_field.top_equiv)