src/HOL/Algebra/Ideal.thy
changeset 68443 43055b016688
parent 67443 3abf6a722518
child 68445 c183a6a69f2d
     1.1 --- a/src/HOL/Algebra/Ideal.thy	Tue Jun 12 11:18:35 2018 +0100
     1.2 +++ b/src/HOL/Algebra/Ideal.thy	Tue Jun 12 16:08:57 2018 +0100
     1.3 @@ -29,7 +29,7 @@
     1.4  lemma idealI:
     1.5    fixes R (structure)
     1.6    assumes "ring R"
     1.7 -  assumes a_subgroup: "subgroup I \<lparr>carrier = carrier R, mult = add R, one = zero R\<rparr>"
     1.8 +  assumes a_subgroup: "subgroup I (add_monoid R)"
     1.9      and I_l_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<otimes> a \<in> I"
    1.10      and I_r_closed: "\<And>a x. \<lbrakk>a \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> a \<otimes> x \<in> I"
    1.11    shows "ideal I R"
    1.12 @@ -708,10 +708,7 @@
    1.13  qed
    1.14  
    1.15  corollary (in cring) domain_eq_zeroprimeideal: "domain R = primeideal {\<zero>} R"
    1.16 -  apply rule
    1.17 -   apply (erule domain.zeroprimeideal)
    1.18 -  apply (erule zeroprimeideal_domainI)
    1.19 -  done
    1.20 +  using domain.zeroprimeideal zeroprimeideal_domainI by blast
    1.21  
    1.22  
    1.23  subsection \<open>Maximal Ideals\<close>
    1.24 @@ -963,9 +960,6 @@
    1.25  qed
    1.26  
    1.27  lemma (in cring) zeromaximalideal_eq_field: "maximalideal {\<zero>} R = field R"
    1.28 -  apply rule
    1.29 -   apply (erule zeromaximalideal_fieldI)
    1.30 -  apply (erule field.zeromaximalideal)
    1.31 -  done
    1.32 +  using field.zeromaximalideal zeromaximalideal_fieldI by blast
    1.33  
    1.34  end