
diff -r d05da6b707dd -r 559f0882d6a6 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Mon Sep 26 07:56:53 2016 +0200
+++ b/src/HOL/Rings.thy	Mon Sep 26 07:56:54 2016 +0200
@@ -1088,6 +1088,20 @@
 lemma mult_one_div_unit_factor [simp]: "a * (1 div unit_factor b) = a div unit_factor b"
   by (cases "b = 0") simp_all
 
+lemma inv_unit_factor_eq_0_iff [simp]:
+  "1 div unit_factor a = 0 \<longleftrightarrow> a = 0"
+  (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  assume ?lhs
+  then have "a * (1 div unit_factor a) = a * 0"
+    by simp
+  then show ?rhs
+    by simp
+next
+  assume ?rhs
+  then show ?lhs by simp
+qed
+
 lemma normalize_mult: "normalize (a * b) = normalize a * normalize b"
 proof (cases "a = 0 \<or> b = 0")
   case True




