proposition: Lemma differentiable_bilin (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) p : continuous (fun p => f p.1 p.2) -> differentiable (fun p => f p.1 p.2) p.
proof: Proof. by move=> fc; apply/diff_locallyP; rewrite diff_bilin //; apply: dbilin p fc. 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