equal
deleted
inserted
replaced
46 lemma StandardRes_prop2: "0 < m ==> (StandardRes m x1 = StandardRes m x2) |
46 lemma StandardRes_prop2: "0 < m ==> (StandardRes m x1 = StandardRes m x2) |
47 = ([x1 = x2] (mod m))" |
47 = ([x1 = x2] (mod m))" |
48 by (auto simp add: StandardRes_def zcong_zmod_eq) |
48 by (auto simp add: StandardRes_def zcong_zmod_eq) |
49 |
49 |
50 lemma StandardRes_prop3: "(~[x = 0] (mod p)) = (~(StandardRes p x = 0))" |
50 lemma StandardRes_prop3: "(~[x = 0] (mod p)) = (~(StandardRes p x = 0))" |
51 by (auto simp add: StandardRes_def zcong_def zdvd_iff_zmod_eq_0) |
51 by (auto simp add: StandardRes_def zcong_def dvd_eq_mod_eq_0) |
52 |
52 |
53 lemma StandardRes_prop4: "2 < m |
53 lemma StandardRes_prop4: "2 < m |
54 ==> [StandardRes m x * StandardRes m y = (x * y)] (mod m)" |
54 ==> [StandardRes m x * StandardRes m y = (x * y)] (mod m)" |
55 by (auto simp add: StandardRes_def zcong_zmod_eq |
55 by (auto simp add: StandardRes_def zcong_zmod_eq |
56 mod_mult_eq [of x y m]) |
56 mod_mult_eq [of x y m]) |