The generator of a simple intermediate field as a root

For an element α of an extension E / F, the generator IntermediateField.AdjoinSimple.gen F α of F⟮α⟯ is a root of a polynomial p over F, viewed over F⟮α⟯, exactly when α is a root of p. This is the form in which a root of p is removed from p over the field it generates.

Main results

• IntermediateField.AdjoinSimple.isRoot_map_gen_iff: the generator of F⟮α⟯ is a root of p mapped to F⟮α⟯ if and only if α is a root of p.

theorem IntermediateField.AdjoinSimple.isRoot_map_gen_iff {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] (α : E) {p : Polynomial F} : (Polynomial.map (algebraMap F ↥F⟮α⟯) p).IsRoot (gen F α) ↔ (Polynomial.aeval α) p = 0

The generator of F⟮α⟯ is a root of p mapped to F⟮α⟯ if and only if α is a root of p.