∀ {K : Type v} {L : Type w} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {f : Polynomial K},
  (Polynomial.map (algebraMap K L) f).Splits → Algebra.adjoin K (f.rootSet L) = ⊤ → Polynomial.IsSplittingField K L f