∀ {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 x_1 : p.Gal) (x_2 : ↑(p.rootSet E)),
  (x * x_1) • x_2 = x • x_1 • x_2