proposition: Lemma derivemxE m n (f : 'rV[R]_m.+1 -> 'rV[R]_n.+1) (a v : 'rV[R]_m.+1) : differentiable f a -> 'D_ v f a = v *m jacobian f a.
proof: Proof. by move=> /deriveE->; rewrite /jacobian mul_rV_lin1. 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