equal
deleted
inserted
replaced
136 lemma SetS_setprod_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p)); |
136 lemma SetS_setprod_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p)); |
137 ~(QuadRes p a); x \<in> (SetS a p) |] ==> |
137 ~(QuadRes p a); x \<in> (SetS a p) |] ==> |
138 [\<Prod>x = a] (mod p)" |
138 [\<Prod>x = a] (mod p)" |
139 apply (auto simp add: SetS_def MultInvPair_def) |
139 apply (auto simp add: SetS_def MultInvPair_def) |
140 apply (frule StandardRes_SRStar_prop1a) |
140 apply (frule StandardRes_SRStar_prop1a) |
|
141 apply hypsubst_thin |
141 apply (subgoal_tac "StandardRes p x \<noteq> StandardRes p (a * MultInv p x)") |
142 apply (subgoal_tac "StandardRes p x \<noteq> StandardRes p (a * MultInv p x)") |
142 apply (auto simp add: StandardRes_prop2 MultInvPair_distinct) |
143 apply (auto simp add: StandardRes_prop2 MultInvPair_distinct) |
143 apply (frule_tac m = p and x = x and y = "(a * MultInv p x)" in |
144 apply (frule_tac m = p and x = x and y = "(a * MultInv p x)" in |
144 StandardRes_prop4) |
145 StandardRes_prop4) |
145 apply (subgoal_tac "[x * (a * MultInv p x) = a * (x * MultInv p x)] (mod p)") |
146 apply (subgoal_tac "[x * (a * MultInv p x) = a * (x * MultInv p x)] (mod p)") |