[STATEMENT]
lemma has_vector_derivative_const[simp, derivative_intros]: "((\<lambda>x. c) has_vector_derivative 0) net"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. c) has_vector_derivative (0::'a)) net
[PROOF STEP]
by (auto simp: has_vector_derivative_def)