src/HOL/Analysis/Complex_Transcendental.thy
changeset 64593 50c715579715
parent 64508 874555896035
child 64773 223b2ebdda79
     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Sat Dec 17 15:22:14 2016 +0100
     1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Sat Dec 17 15:22:14 2016 +0100
     1.3 @@ -3206,7 +3206,7 @@
     1.4        using of_int_eq_iff apply fastforce
     1.5        by (metis of_int_add of_int_mult of_int_of_nat_eq)
     1.6      also have "... \<longleftrightarrow> int j mod int n = int k mod int n"
     1.7 -      by (auto simp: zmod_eq_dvd_iff dvd_def algebra_simps)
     1.8 +      by (auto simp: mod_eq_dvd_iff dvd_def algebra_simps)
     1.9      also have "... \<longleftrightarrow> j mod n = k mod n"
    1.10        by (metis of_nat_eq_iff zmod_int)
    1.11      finally have "(\<exists>z. \<i> * (of_nat j * (of_real pi * 2)) =