src/HOL/Algebra/QuotRing.thy
changeset 23463 9953ff53cc64
parent 23350 50c5b0912a0c
child 27611 2c01c0bdb385
     1.1 --- a/src/HOL/Algebra/QuotRing.thy	Thu Jun 21 17:28:50 2007 +0200
     1.2 +++ b/src/HOL/Algebra/QuotRing.thy	Thu Jun 21 17:28:53 2007 +0200
     1.3 @@ -4,17 +4,17 @@
     1.4    Author:    Stephan Hohe
     1.5  *)
     1.6  
     1.7 +header {* Quotient Rings *}
     1.8 +
     1.9  theory QuotRing
    1.10  imports RingHom
    1.11  begin
    1.12  
    1.13 -
    1.14 -section {* Quotient Rings *}
    1.15 -
    1.16  subsection {* Multiplication on Cosets *}
    1.17  
    1.18  constdefs (structure R)
    1.19 -  rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set"   ("[mod _:] _ \<Otimes>\<index> _" [81,81,81] 80)
    1.20 +  rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set"
    1.21 +    ("[mod _:] _ \<Otimes>\<index> _" [81,81,81] 80)
    1.22    "rcoset_mult R I A B \<equiv> \<Union>a\<in>A. \<Union>b\<in>B. I +> (a \<otimes> b)"
    1.23  
    1.24  
    1.25 @@ -171,8 +171,9 @@
    1.26    shows "ring_hom_cring R (R Quot I) (op +> I)"
    1.27  apply (rule ring_hom_cringI)
    1.28    apply (rule rcos_ring_hom_ring)
    1.29 - apply assumption
    1.30 -apply (rule quotient_is_cring, assumption)
    1.31 + apply (rule R.is_cring)
    1.32 +apply (rule quotient_is_cring)
    1.33 +apply (rule R.is_cring)
    1.34  done
    1.35  
    1.36