∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : CommRing S] [inst_3 : Algebra S R]
  {G : Type u_1} [inst_4 : Monoid G] [inst_5 : MulSemiringAction G R] [inst_6 : SMulCommClass G S R] {f : Polynomial S}
  (g : G) (x : ↑(f.rootSet R)), g • ↑x = ↑(g • x)