src/HOL/Algebra/QuotRing.thy
 changeset 27611 2c01c0bdb385 parent 23463 9953ff53cc64 child 27717 21bbd410ba04
```     1.1 --- a/src/HOL/Algebra/QuotRing.thy	Tue Jul 15 16:02:10 2008 +0200
1.2 +++ b/src/HOL/Algebra/QuotRing.thy	Tue Jul 15 16:50:09 2008 +0200
1.3 @@ -155,27 +155,32 @@
1.4
1.5  text {* The quotient of a cring is also commutative *}
1.6  lemma (in ideal) quotient_is_cring:
1.7 -  includes cring
1.8 +  assumes "cring R"
1.9    shows "cring (R Quot I)"
1.10 -apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro)
1.11 +proof -
1.12 +  interpret cring [R] by fact
1.13 +  show ?thesis apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro)
1.14    apply (rule quotient_is_ring)
1.15   apply (rule ring.axioms[OF quotient_is_ring])
1.16  apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric])
1.17  apply clarify
1.18  apply (simp add: rcoset_mult_add m_comm)
1.19  done
1.20 +qed
1.21
1.22  text {* Cosets as a ring homomorphism on crings *}
1.23  lemma (in ideal) rcos_ring_hom_cring:
1.24 -  includes cring
1.25 +  assumes "cring R"
1.26    shows "ring_hom_cring R (R Quot I) (op +> I)"
1.27 -apply (rule ring_hom_cringI)
1.28 +proof -
1.29 +  interpret cring [R] by fact
1.30 +  show ?thesis apply (rule ring_hom_cringI)
1.31    apply (rule rcos_ring_hom_ring)
1.32   apply (rule R.is_cring)
1.33  apply (rule quotient_is_cring)
1.34  apply (rule R.is_cring)
1.35  done
1.36 -
1.37 +qed
1.38
1.39  subsection {* Factorization over Prime Ideals *}
1.40
1.41 @@ -236,9 +241,11 @@
1.42          The proof follows ``W. Adkins, S. Weintraub: Algebra --
1.43          An Approach via Module Theory'' *}
1.44  lemma (in maximalideal) quotient_is_field:
1.45 -  includes cring
1.46 +  assumes "cring R"
1.47    shows "field (R Quot I)"
1.48 -apply (intro cring.cring_fieldI2)
1.49 +proof -
1.50 +  interpret cring [R] by fact
1.51 +  show ?thesis apply (intro cring.cring_fieldI2)
1.52    apply (rule quotient_is_cring, rule is_cring)
1.53   defer 1
1.54   apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarsimp)
1.55 @@ -338,5 +345,6 @@
1.56    from rcarr and this[symmetric]
1.57    show "\<exists>r\<in>carrier R. I +> a \<otimes> r = I +> \<one>" by fast
1.58  qed
1.59 +qed
1.60
1.61  end
```