--- a/src/HOL/Deriv.thy Thu Jul 15 22:51:49 2021 +0200
+++ b/src/HOL/Deriv.thy Fri Jul 16 14:43:25 2021 +0100
@@ -959,6 +959,12 @@
shows "(f has_vector_derivative x) F \<Longrightarrow> ((\<lambda>x. f x * a) has_vector_derivative (x * a)) F"
by (rule bounded_linear.has_vector_derivative[OF bounded_linear_mult_left])
+lemma has_vector_derivative_divide[derivative_intros]:
+ fixes a :: "'a::real_normed_field"
+ shows "(f has_vector_derivative x) F \<Longrightarrow> ((\<lambda>x. f x / a) has_vector_derivative (x / a)) F"
+ using has_vector_derivative_mult_left [of f x F "inverse a"]
+ by (simp add: field_class.field_divide_inverse)
+
subsection \<open>Derivatives\<close>