∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid S] [inst_2 : SMulWithZero R S]
  [inst_3 : Monoid S] (x : Sˣ) (n : ℤ) (r : R), LaurentPolynomial.smeval (AddMonoidAlgebra.single n r) x = r • ↑(x ^ n)