∀ {R : Type u_11} {V : Type u} {E : Type v} {F : outParam (Type w)} {inst : SMul R V} {inst_1 : SMul R F}
  {inst_2 : LineDeriv V E F} [self : LineDerivLeftSMul R V E F] (r : R) (v : V) (x : E),
  LineDeriv.lineDerivOp (r • v) x = r • LineDeriv.lineDerivOp v x