∀ {F : Type u} {K : Type v} [inst : CommRing K] [inst_1 : Field F] {L : Type u_2} [inst_2 : CommRing L] (i : K →+* L)
  (j : L →+* F) {f : Polynomial K},
  (Polynomial.map j (Polynomial.map i f)).Splits ↔ (Polynomial.map (j.comp i) f).Splits