equal
deleted
inserted
replaced
1617 |
1617 |
1618 lemma dvd_mod_imp_dvd: |
1618 lemma dvd_mod_imp_dvd: |
1619 assumes "c dvd a mod b" and "c dvd b" |
1619 assumes "c dvd a mod b" and "c dvd b" |
1620 shows "c dvd a" |
1620 shows "c dvd a" |
1621 using assms dvd_mod_iff [of c b a] by simp |
1621 using assms dvd_mod_iff [of c b a] by simp |
|
1622 |
|
1623 lemma dvd_minus_mod [simp]: |
|
1624 "b dvd a - a mod b" |
|
1625 by (simp add: minus_mod_eq_div_mult) |
1622 |
1626 |
1623 end |
1627 end |
1624 |
1628 |
1625 class idom_modulo = idom + semidom_modulo |
1629 class idom_modulo = idom + semidom_modulo |
1626 begin |
1630 begin |