∀ {F : Type u_2} [inst : Field F] (p : Polynomial F) (E : Type u_1) [inst_1 : Field E] [inst_2 : Algebra F E]
  [inst_3 : Fact (Polynomial.map (algebraMap F E) p).Splits] (x : ↑(p.rootSet E)), 1 • x = x