src/HOL/Rings.thy
changeset 68252 8b284d24f434
parent 68251 54a127873735
child 68253 a8660a39e304
equal deleted inserted replaced
68251:54a127873735 68252:8b284d24f434
  1710 
  1710 
  1711 lemma dvd_imp_mod_0 [simp]:
  1711 lemma dvd_imp_mod_0 [simp]:
  1712   "b mod a = 0" if "a dvd b"
  1712   "b mod a = 0" if "a dvd b"
  1713   using that minus_div_mult_eq_mod [of b a] by simp
  1713   using that minus_div_mult_eq_mod [of b a] by simp
  1714 
  1714 
  1715 lemma mod_0_imp_dvd: 
  1715 lemma mod_0_imp_dvd [dest!]: 
  1716   "b dvd a" if "a mod b = 0"
  1716   "b dvd a" if "a mod b = 0"
  1717 proof -
  1717 proof -
  1718   have "b dvd (a div b) * b" by simp
  1718   have "b dvd (a div b) * b" by simp
  1719   also have "(a div b) * b = a"
  1719   also have "(a div b) * b = a"
  1720     using div_mult_mod_eq [of a b] by (simp add: that)
  1720     using div_mult_mod_eq [of a b] by (simp add: that)