src/HOL/Analysis/Complex_Transcendental.thy
 changeset 64240 eabf80376aab parent 63918 6bf55e6e0b75 child 64267 b9a1486e79be
```     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Sun Oct 16 09:31:03 2016 +0200
1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Sun Oct 16 09:31:04 2016 +0200
1.3 @@ -1315,7 +1315,7 @@
1.4    case False
1.5    then have "z / of_real(norm z) = exp(\<i> * of_real(Arg z))"
1.6      using Arg [of z]
1.7 -    by (metis abs_norm_cancel nonzero_mult_divide_cancel_left norm_of_real zero_less_norm_iff)
1.8 +    by (metis abs_norm_cancel nonzero_mult_div_cancel_left norm_of_real zero_less_norm_iff)
1.9    then have "- z / of_real(norm z) = exp (\<i> * (of_real (Arg z) - pi))"
1.10      using cis_conv_exp cis_pi
1.11      by (auto simp: exp_diff algebra_simps)
1.12 @@ -1918,7 +1918,7 @@
1.13      shows "csqrt z = exp(Ln(z) / 2)"
1.14  proof -
1.15    have "(exp (Ln z / 2))\<^sup>2 = (exp (Ln z))"
1.16 -    by (metis exp_double nonzero_mult_divide_cancel_left times_divide_eq_right zero_neq_numeral)
1.17 +    by (metis exp_double nonzero_mult_div_cancel_left times_divide_eq_right zero_neq_numeral)
1.18    also have "... = z"
1.19      using assms exp_Ln by blast
1.20    finally have "csqrt z = csqrt ((exp (Ln z / 2))\<^sup>2)"
```