∀ {M : Type u_3} [inst : Monoid M] {P : Type u_2} [inst_1 : CommSemiring P] [inst_2 : MulSemiringAction M P]
  {Q : Type u_1} [inst_3 : CommSemiring Q] [inst_4 : MulSemiringAction M Q] (g : P →+*[M] Q), Polynomial.map (↑g) 0 = 0