src/HOL/Rings.thy
changeset 68251 54a127873735
parent 67689 2c38ffd6ec71
child 68252 8b284d24f434
equal deleted inserted replaced
68250:c45067867860 68251:54a127873735
   135   where "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
   135   where "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
   136 
   136 
   137 lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"
   137 lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"
   138   unfolding dvd_def ..
   138   unfolding dvd_def ..
   139 
   139 
   140 lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P"
   140 lemma dvdE [elim]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P"
   141   unfolding dvd_def by blast
   141   unfolding dvd_def by blast
   142 
   142 
   143 end
   143 end
   144 
   144 
   145 context comm_monoid_mult
   145 context comm_monoid_mult