Primitive element of a field extension (source code)

= Primitive element of a field extension

A primitive element of a finite extension $L/K$ is an element $\alpha\in L$ such that $L=K(\alpha)$.

The <primitive element theorem> proves existence under finite separability; the <primitive element of a field extension> is the generator whose existence the theorem asserts.