Extension theorem for field embeddings
= Extension theorem for field embeddings
An embedding of a subfield into an algebraically closed field extends over an algebraic extension: for a simple extension, map its generator to a root of the transported <minimal polynomial>, then iterate or use <Zorn lemma>. If the larger extension is normal over the fixed base, its image under the extended embedding is itself.