src/HOL/Complex.thy
changeset 61848 9250e546ab23
parent 61799 4cf66f21b764
child 61944 5d06ecfdb472
     1.1 --- a/src/HOL/Complex.thy	Mon Dec 14 14:05:31 2015 +0100
     1.2 +++ b/src/HOL/Complex.thy	Tue Dec 15 14:40:36 2015 +0000
     1.3 @@ -784,7 +784,10 @@
     1.4    apply (rule_tac x = "ii * complex_of_real a" in exI, auto)
     1.5    done
     1.6  
     1.7 -lemma exp_two_pi_i [simp]: "exp(2 * complex_of_real pi * ii) = 1"
     1.8 +lemma exp_pi_i [simp]: "exp(of_real pi * ii) = -1"
     1.9 +  by (metis cis_conv_exp cis_pi mult.commute)
    1.10 +
    1.11 +lemma exp_two_pi_i [simp]: "exp(2 * of_real pi * ii) = 1"
    1.12    by (simp add: exp_eq_polar complex_eq_iff)
    1.13  
    1.14  subsubsection \<open>Complex argument\<close>