equal
deleted
inserted
replaced
1080 zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard] |
1080 zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard] |
1081 |
1081 |
1082 lemma zdvd_0_right [iff]: "(m::int) dvd 0" |
1082 lemma zdvd_0_right [iff]: "(m::int) dvd 0" |
1083 by (simp add: dvd_def) |
1083 by (simp add: dvd_def) |
1084 |
1084 |
1085 lemma zdvd_0_left [iff]: "(0 dvd (m::int)) = (m = 0)" |
1085 lemma zdvd_0_left [iff,noatp]: "(0 dvd (m::int)) = (m = 0)" |
1086 by (simp add: dvd_def) |
1086 by (simp add: dvd_def) |
1087 |
1087 |
1088 lemma zdvd_1_left [iff]: "1 dvd (m::int)" |
1088 lemma zdvd_1_left [iff]: "1 dvd (m::int)" |
1089 by (simp add: dvd_def) |
1089 by (simp add: dvd_def) |
1090 |
1090 |