∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {F : Type u_6}
  [inst_3 : Field F] [inst_4 : Algebra K F] (x : L),
  (Polynomial.map (algebraMap K F) (minpoly K x)).Splits →
    (algebraMap K F) ((Algebra.trace K ↥K⟮x⟯) (IntermediateField.AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).sum