src/HOL/Complex.thy
changeset 63114 27afe7af7379
parent 63040 eb4ddd18d635
child 63569 7e0b0db5e9ac
     1.1 --- a/src/HOL/Complex.thy	Sat May 21 07:08:59 2016 +0200
     1.2 +++ b/src/HOL/Complex.thy	Mon May 23 15:33:24 2016 +0100
     1.3 @@ -799,9 +799,15 @@
     1.4  lemma exp_pi_i [simp]: "exp(of_real pi * ii) = -1"
     1.5    by (metis cis_conv_exp cis_pi mult.commute)
     1.6  
     1.7 +lemma exp_pi_i' [simp]: "exp(ii * of_real pi) = -1"
     1.8 +  using cis_conv_exp cis_pi by auto
     1.9 +
    1.10  lemma exp_two_pi_i [simp]: "exp(2 * of_real pi * ii) = 1"
    1.11    by (simp add: exp_eq_polar complex_eq_iff)
    1.12  
    1.13 +lemma exp_two_pi_i' [simp]: "exp (\<i> * (of_real pi * 2)) = 1"
    1.14 +  by (metis exp_two_pi_i mult.commute)
    1.15 +
    1.16  subsubsection \<open>Complex argument\<close>
    1.17  
    1.18  definition arg :: "complex \<Rightarrow> real" where