--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy Wed May 26 18:07:49 2021 +0200
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy Fri May 28 14:43:06 2021 +0100
@@ -2482,12 +2482,13 @@
theorem Liouville_theorem:
assumes holf: "f holomorphic_on UNIV"
and bf: "bounded (range f)"
- obtains c where "\<And>z. f z = c"
+ shows "f constant_on UNIV"
proof -
obtain B where "\<And>z. cmod (f z) \<le> B"
by (meson bf bounded_pos rangeI)
then show ?thesis
- using Liouville_polynomial [OF holf, of 0 B 0, simplified] that by blast
+ using Liouville_polynomial [OF holf, of 0 B 0, simplified]
+ by (meson constant_on_def)
qed
text\<open>A holomorphic function f has only isolated zeros unless f is 0.\<close>