diff -r 6621d91d3c8a -r 240a39af9ec4 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Fields.thy	Sat Dec 17 15:22:13 2016 +0100
@@ -506,6 +506,21 @@
   "y \<noteq> 0 \<Longrightarrow> z + x / y = (x + z * y) / y"
   by (simp add: add_divide_distrib add.commute)
 
+lemma dvd_field_iff:
+  "a dvd b \<longleftrightarrow> (a = 0 \<longrightarrow> b = 0)"
+proof (cases "a = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  then have "b = a * (b / a)"
+    by (simp add: field_simps)
+  then have "a dvd b" ..
+  with False show ?thesis
+    by simp
+qed
+
 end
 
 class field_char_0 = field + ring_char_0