--- a/src/HOL/Complex.thy Mon Dec 14 14:05:31 2015 +0100
+++ b/src/HOL/Complex.thy Tue Dec 15 14:40:36 2015 +0000
@@ -784,7 +784,10 @@
apply (rule_tac x = "ii * complex_of_real a" in exI, auto)
done
-lemma exp_two_pi_i [simp]: "exp(2 * complex_of_real pi * ii) = 1"
+lemma exp_pi_i [simp]: "exp(of_real pi * ii) = -1"
+ by (metis cis_conv_exp cis_pi mult.commute)
+
+lemma exp_two_pi_i [simp]: "exp(2 * of_real pi * ii) = 1"
by (simp add: exp_eq_polar complex_eq_iff)
subsubsection \<open>Complex argument\<close>