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