∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (i : ℕ)
  (f : Polynomial R) (m : M) (n : ℕ), (f • (PolynomialModule.single R i) m) n = if i ≤ n then f.coeff (n - i) • m else 0