diff -r 9a60c1759543 -r 0fb350e7477b src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Tue Jan 31 14:05:16 2023 +0000
+++ b/src/HOL/Analysis/Derivative.thy	Wed Feb 01 12:43:33 2023 +0000
@@ -2104,6 +2104,12 @@
   using assms unfolding field_differentiable_def
   by (metis DERIV_power)
 
+lemma field_differentiable_cnj_cnj:
+  assumes "f field_differentiable (at (cnj z))"
+  shows   "(cnj \<circ> f \<circ> cnj) field_differentiable (at z)"
+  using has_field_derivative_cnj_cnj assms
+  by (auto simp: field_differentiable_def)
+ 
 lemma field_differentiable_transform_within:
   "0 < d \<Longrightarrow>
         x \<in> S \<Longrightarrow>