src/HOL/Multivariate_Analysis/Derivative.thy

--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Jul 20 11:40:43 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Jul 20 23:12:50 2015 +0100
@@ -2312,4 +2312,7 @@
   apply (simp only: o_def real_scaleR_def scaleR_scaleR)
   done
 
+lemma vector_derivative_const_at [simp]: "vector_derivative (\<lambda>x. c) (at a) = 0"
+  by (simp add: vector_derivative_at)
+
 end