∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : AddCommGroup M] [inst_4 : Module A M] [inst_5 : Module R M] (d : Derivation R A M) (x : A),
  d.mapCoeffs (Polynomial.C x) = (PolynomialModule.single A 0) (d x)