proposition: Lemma differentiable_coord m n (M : 'M[R]_(m.+1, n.+1)) i j : differentiable (fun N : 'M[R]_(m.+1, n.+1) => N i j : R ) M.
proof: Proof. have @f : {linear 'M[R]_(m.+1, n.+1) -> R}. by exists (fun N : 'M[R]_(_, _) => N i j); do 2![eexists]; do ?[constructor]; rewrite ?mxE// => ? *; rewrite ?mxE//; move=> ?; rewrite !mxE. rewrite (_ : (fun _ => _) = f) //; exact/linear_differentiable/coord_continuous. 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