∀ {T : Type u_2} {S : Type u_3} [inst : CommRing T] [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra T S]
  {a b c : T} {x1 x2 : S},
  (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).aroots S = {x1, x2} →
    (algebraMap T S) b = -(algebraMap T S) a * (x1 + x2)