src/HOL/Rings.thy
changeset 36719 d396f6f63d94
parent 36622 e393a91f86df
child 36821 9207505d1ee5
     1.1 --- a/src/HOL/Rings.thy	Thu May 06 19:35:43 2010 +0200
     1.2 +++ b/src/HOL/Rings.thy	Thu May 06 23:11:56 2010 +0200
     1.3 @@ -183,9 +183,21 @@
     1.4  
     1.5  end
     1.6  
     1.7 -
     1.8  class no_zero_divisors = zero + times +
     1.9    assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
    1.10 +begin
    1.11 +
    1.12 +lemma divisors_zero:
    1.13 +  assumes "a * b = 0"
    1.14 +  shows "a = 0 \<or> b = 0"
    1.15 +proof (rule classical)
    1.16 +  assume "\<not> (a = 0 \<or> b = 0)"
    1.17 +  then have "a \<noteq> 0" and "b \<noteq> 0" by auto
    1.18 +  with no_zero_divisors have "a * b \<noteq> 0" by blast
    1.19 +  with assms show ?thesis by simp
    1.20 +qed
    1.21 +
    1.22 +end
    1.23  
    1.24  class semiring_1_cancel = semiring + cancel_comm_monoid_add
    1.25    + zero_neq_one + monoid_mult