src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
changeset 60809 457abb82fb9e
parent 60420 884f54e01427
child 61070 b72a990adfe2
     1.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Jul 28 13:00:54 2015 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Jul 28 16:16:13 2015 +0100
     1.3 @@ -1448,15 +1448,15 @@
     1.4    fixes n::nat and z::complex shows "z powr n = (if z = 0 then 0 else z^n)"
     1.5    by (simp add: exp_of_nat_mult powr_def)
     1.6  
     1.7 -lemma powr_add:
     1.8 +lemma powr_add_complex:
     1.9    fixes w::complex shows "w powr (z1 + z2) = w powr z1 * w powr z2"
    1.10    by (simp add: powr_def algebra_simps exp_add)
    1.11  
    1.12 -lemma powr_minus:
    1.13 +lemma powr_minus_complex:
    1.14    fixes w::complex shows  "w powr (-z) = inverse(w powr z)"
    1.15    by (simp add: powr_def exp_minus)
    1.16  
    1.17 -lemma powr_diff:
    1.18 +lemma powr_diff_complex:
    1.19    fixes w::complex shows  "w powr (z1 - z2) = w powr z1 / w powr z2"
    1.20    by (simp add: powr_def algebra_simps exp_diff)
    1.21