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))"