src/HOL/Number_Theory/Euler_Criterion.thy
changeset 67051 e7e54a0b9197
parent 66888 930abfdf8727
child 67083 6b2c0681ef28
     1.1 --- a/src/HOL/Number_Theory/Euler_Criterion.thy	Sat Nov 11 18:33:35 2017 +0000
     1.2 +++ b/src/HOL/Number_Theory/Euler_Criterion.thy	Sat Nov 11 18:41:08 2017 +0000
     1.3 @@ -65,7 +65,7 @@
     1.4  proof -
     1.5    have "~ p dvd x" using assms zdvd_not_zless S1_def by auto
     1.6    hence co_xp: "coprime x p" using p_prime prime_imp_coprime_int[of p x] 
     1.7 -    by (simp add: gcd.commute)
     1.8 +    by (simp add: ac_simps)
     1.9    then obtain y' where y': "[x * y' = 1] (mod p)" using cong_solve_coprime_int by blast
    1.10    moreover define y where "y = y' * a mod p"
    1.11    ultimately have "[x * y = a] (mod p)" using mod_mult_right_eq[of x "y' * a" p]