src/HOL/Rings.thy
changeset 63947 559f0882d6a6
parent 63924 f91766530e13
child 63950 cdc1e59aa513
     1.1 --- a/src/HOL/Rings.thy	Mon Sep 26 07:56:53 2016 +0200
     1.2 +++ b/src/HOL/Rings.thy	Mon Sep 26 07:56:54 2016 +0200
     1.3 @@ -1088,6 +1088,20 @@
     1.4  lemma mult_one_div_unit_factor [simp]: "a * (1 div unit_factor b) = a div unit_factor b"
     1.5    by (cases "b = 0") simp_all
     1.6  
     1.7 +lemma inv_unit_factor_eq_0_iff [simp]:
     1.8 +  "1 div unit_factor a = 0 \<longleftrightarrow> a = 0"
     1.9 +  (is "?lhs \<longleftrightarrow> ?rhs")
    1.10 +proof
    1.11 +  assume ?lhs
    1.12 +  then have "a * (1 div unit_factor a) = a * 0"
    1.13 +    by simp
    1.14 +  then show ?rhs
    1.15 +    by simp
    1.16 +next
    1.17 +  assume ?rhs
    1.18 +  then show ?lhs by simp
    1.19 +qed
    1.20 +
    1.21  lemma normalize_mult: "normalize (a * b) = normalize a * normalize b"
    1.22  proof (cases "a = 0 \<or> b = 0")
    1.23    case True