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
```