src/HOL/Rings.thy
changeset 63359 99b51ba8da1c
parent 63325 1086d56cde86
child 63456 3365c8ec67bd
     1.1 --- a/src/HOL/Rings.thy	Fri Jul 01 08:19:53 2016 +0200
     1.2 +++ b/src/HOL/Rings.thy	Fri Jul 01 08:35:15 2016 +0200
     1.3 @@ -757,6 +757,17 @@
     1.4    finally show ?thesis .
     1.5  qed
     1.6  
     1.7 +lemma dvd_mult_imp_div:
     1.8 +  assumes "a * c dvd b"
     1.9 +  shows "a dvd b div c"
    1.10 +proof (cases "c = 0")
    1.11 +  case True then show ?thesis by simp
    1.12 +next
    1.13 +  case False
    1.14 +  from \<open>a * c dvd b\<close> obtain d where "b = a * c * d" ..
    1.15 +  with False show ?thesis by (simp add: mult.commute [of a] mult.assoc)
    1.16 +qed
    1.17 +
    1.18  
    1.19  text \<open>Units: invertible elements in a ring\<close>
    1.20