proposition: Lemma diffZl (k : V -> R) (f : W) x : differentiable k x -> 'd (fun z => k z *: f) x = (fun z => 'd k x z *: f) :> (_ -> _).
proof: Proof. move=> df; set g := RHS; have glin : linear g. by move=> a u v; rewrite /g linearP /= scalerDl -scalerA. pose glM := GRing.isLinear.Build _ _ _ _ _ glin. pose gL : {linear _ -> _} := HB.pack g glM. by apply:(@diff_unique _ _ _ gL); have [] := dscalel f df. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix interval) mathcomp(mathcomp_extra boolp classical_sets functions) reals signed topology prodnormedzmodule normedtype landau forms