src/HOL/Algebra/Ring.thy
changeset 68551 b680e74eb6f2
parent 68517 6b5f15387353
child 68552 391e89e03eef
     1.1 --- a/src/HOL/Algebra/Ring.thy	Fri Jun 29 23:04:36 2018 +0200
     1.2 +++ b/src/HOL/Algebra/Ring.thy	Sat Jun 30 15:44:04 2018 +0100
     1.3 @@ -333,11 +333,6 @@
     1.4      and "\<And>x y z. \<lbrakk> x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk> \<Longrightarrow> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
     1.5    using assms cring_def apply auto by (simp add: assms cring.axioms(1) ringE(3))
     1.6  
     1.7 -(*
     1.8 -lemma (in cring) is_comm_monoid:
     1.9 -  "comm_monoid R"
    1.10 -  by (auto intro!: comm_monoidI m_assoc m_comm)
    1.11 -*)
    1.12  lemma (in cring) is_cring:
    1.13    "cring R" by (rule cring_axioms)
    1.14  
    1.15 @@ -652,6 +647,15 @@
    1.16  text \<open>Field would not need to be derived from domain, the properties
    1.17    for domain follow from the assumptions of field\<close>
    1.18  
    1.19 +lemma fieldE :
    1.20 +  fixes R (structure)
    1.21 +  assumes "field R"
    1.22 +  shows "cring R"
    1.23 +    and one_not_zero : "\<one> \<noteq> \<zero>"
    1.24 +    and integral: "\<And>a b. \<lbrakk> a \<otimes> b = \<zero>; a \<in> carrier R; b \<in> carrier R \<rbrakk> \<Longrightarrow> a = \<zero> \<or> b = \<zero>"
    1.25 +  and field_Units: "Units R = carrier R - {\<zero>}"
    1.26 +  using assms unfolding field_def field_axioms_def domain_def domain_axioms_def by simp_all
    1.27 +
    1.28  lemma (in cring) cring_fieldI:
    1.29    assumes field_Units: "Units R = carrier R - {\<zero>}"
    1.30    shows "field R"