∀ {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}
  [inst_7 : DecidableEq ↑(f.rootSet S)],
  (Polynomial.map (algebraMap R S) f).Splits →
    ∀ (p : Ideal S) [inst_8 : p.IsPrime],
      (f.rootSet S).ncard ≤ (f.rootSet (S ⧸ p)).ncard + 1 →
        ∀ g ∈ Ideal.inertia G p,
          (MulAction.toPermHom G ↑(f.rootSet S)) g = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) g).IsSwap