proposition: Fact dscalel (k : V -> R) (f : W) x : differentiable k x -> continuous (fun z : V => 'd k x z *: f) /\ (fun z => k z *: f) \o shift x = cst (k x *: f) + (fun z => 'd k x z *: f) +o_ (0 : V) id.
proof: Proof. move=> df; split. move=> ?; exact/continuousZl/diff_continuous. apply/eqaddoE; rewrite funeqE => y /=. by rewrite diff_locallyx //= !scalerDl scaleolx. 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