src/HOL/Old_Number_Theory/WilsonRuss.thy
changeset 47163 248376f8881d
parent 44821 a92f65e174cf
child 47164 6a4c479ba94f
     1.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Tue Mar 27 15:40:11 2012 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Tue Mar 27 15:53:48 2012 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4      "zprime p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> [a * inv p a = 1] (mod p)"
     1.5    apply (unfold inv_def)
     1.6    apply (subst zcong_zmod)
     1.7 -  apply (subst zmod_zmult1_eq [symmetric])
     1.8 +  apply (subst mod_mult_right_eq [symmetric])
     1.9    apply (subst zcong_zmod [symmetric])
    1.10    apply (subst power_Suc [symmetric])
    1.11    apply (subst inv_is_inv_aux)