{F : Type u_1} →
  [inst : Field F] →
    (p : Polynomial F) →
      (E : Type u_2) →
        [inst_1 : Field E] →
          [inst_2 : Algebra F E] → [h : Fact (Polynomial.map (algebraMap F E) p).Splits] → Algebra p.SplittingField E