990 assumes z: "z \<noteq> 0" |
990 assumes z: "z \<noteq> 0" |
991 shows "ln (cmod z) \<le> cmod (Ln z)" |
991 shows "ln (cmod z) \<le> cmod (Ln z)" |
992 using norm_exp [of "Ln z", simplified exp_Ln [OF z]] |
992 using norm_exp [of "Ln z", simplified exp_Ln [OF z]] |
993 by (metis Re_Ln complex_Re_le_cmod z) |
993 by (metis Re_Ln complex_Re_le_cmod z) |
994 |
994 |
995 lemma exists_complex_root: |
995 proposition exists_complex_root: |
996 fixes a :: complex |
996 fixes z :: complex |
997 shows "n \<noteq> 0 \<Longrightarrow> \<exists>z. z ^ n = a" |
997 assumes "n \<noteq> 0" obtains w where "z = w ^ n" |
998 apply (cases "a=0", simp) |
998 apply (cases "z=0") |
999 apply (rule_tac x= "exp(Ln(a) / n)" in exI) |
999 using assms apply (simp add: power_0_left) |
1000 apply (auto simp: exp_of_nat_mult [symmetric]) |
1000 apply (rule_tac w = "exp(Ln z / n)" in that) |
1001 done |
1001 apply (auto simp: assms exp_of_nat_mult [symmetric]) |
|
1002 done |
|
1003 |
|
1004 corollary exists_complex_root_nonzero: |
|
1005 fixes z::complex |
|
1006 assumes "z \<noteq> 0" "n \<noteq> 0" |
|
1007 obtains w where "w \<noteq> 0" "z = w ^ n" |
|
1008 by (metis exists_complex_root [of n z] assms power_0_left) |
1002 |
1009 |
1003 subsection\<open>The Unwinding Number and the Ln-product Formula\<close> |
1010 subsection\<open>The Unwinding Number and the Ln-product Formula\<close> |
1004 |
1011 |
1005 text\<open>Note that in this special case the unwinding number is -1, 0 or 1.\<close> |
1012 text\<open>Note that in this special case the unwinding number is -1, 0 or 1.\<close> |
1006 |
1013 |