equal
deleted
inserted
replaced
1044 |
1044 |
1045 subsection {* The Divides Relation *} |
1045 subsection {* The Divides Relation *} |
1046 |
1046 |
1047 lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))" |
1047 lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))" |
1048 by(simp add:dvd_def zmod_eq_0_iff) |
1048 by(simp add:dvd_def zmod_eq_0_iff) |
|
1049 |
|
1050 declare zdvd_iff_zmod_eq_0[of "number_of x" "number_of y", standard, simp] |
1049 |
1051 |
1050 lemma zdvd_0_right [iff]: "(m::int) dvd 0" |
1052 lemma zdvd_0_right [iff]: "(m::int) dvd 0" |
1051 by (simp add: dvd_def) |
1053 by (simp add: dvd_def) |
1052 |
1054 |
1053 lemma zdvd_0_left [iff]: "(0 dvd (m::int)) = (m = 0)" |
1055 lemma zdvd_0_left [iff]: "(0 dvd (m::int)) = (m = 0)" |