∀ {R : Type u_1} [inst : Semiring R] (r : R) {S : Type u_2} [inst_1 : AddCommMonoid S] [inst_2 : Pow S ℕ]
  [inst_3 : MulActionWithZero R S] (x : S) (n : ℕ), ((Polynomial.monomial n) r).smeval x = r • x ^ n