src/HOL/Old_Number_Theory/WilsonRuss.thy
changeset 61649 268d88ec9087
parent 61382 efac889fccbc
child 61694 6571c78c9667
     1.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Thu Nov 12 11:22:26 2015 +0100
     1.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Fri Nov 13 12:27:13 2015 +0000
     1.3 @@ -133,7 +133,7 @@
     1.4      5 \<le> p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a"
     1.5    apply (unfold inv_def)
     1.6    apply (subst power_mod)
     1.7 -  apply (subst zpower_zpower)
     1.8 +  apply (subst power_mult [symmetric])
     1.9    apply (rule zcong_zless_imp_eq)
    1.10        prefer 5
    1.11        apply (subst zcong_zmod)