src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy
changeset 82517 111b1b2a2d13
parent 82461 eea85bbd2feb
child 82534 34190188b40f
child 82538 4b132ea7d575
--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy	Tue Apr 15 23:04:44 2025 +0200
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy	Tue Apr 15 15:17:25 2025 +0200
@@ -468,7 +468,7 @@
   thus ?thesis
     by (simp add: o_def)
 qed
-    
+
 lemma contour_integral_comp_analyticW:
   assumes "f analytic_on s" "valid_path \<gamma>" "path_image \<gamma> \<subseteq> s"
   shows "contour_integral (f \<circ> \<gamma>) g = contour_integral \<gamma> (\<lambda>w. deriv f w * g (f w))"