∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : IsDomain S]
  {G : Type u_3} [inst_4 : Group G] [inst_5 : MulSemiringAction G S] [inst_6 : SMulCommClass G R S] {f : Polynomial R},
  (Polynomial.map (algebraMap R S) f).Splits →
    ∀ [MulAction.IsPretransitive G ↑(f.rootSet S)],
      (∀ (m : MaximalSpectrum S), (f.rootSet S).ncard ≤ (f.rootSet (S ⧸ m.asIdeal)).ncard + 1) →
        ⨆ m, Ideal.inertia G m.asIdeal = ⊤ → Function.Surjective ⇑(MulAction.toPermHom G ↑(f.rootSet S))