∀ (A : Type u_2) [inst : CommSemiring A] {B : Type u_3} [inst_1 : Semiring B] [inst_2 : Algebra A B] (P : Ideal B)
  {G : Type u_5} [inst_3 : Group G] [inst_4 : MulSemiringAction G B] [SMulCommClass G A B] (g : G),
  Ideal.under A (g • P) = Ideal.under A P