equal
deleted
inserted
replaced
9 |
9 |
10 section {* Quotient Rings *} |
10 section {* Quotient Rings *} |
11 |
11 |
12 subsection {* Multiplication on Cosets *} |
12 subsection {* Multiplication on Cosets *} |
13 |
13 |
14 constdefs (structure R) |
14 definition |
15 rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set" |
15 rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set" |
16 ("[mod _:] _ \<Otimes>\<index> _" [81,81,81] 80) |
16 ("[mod _:] _ \<Otimes>\<index> _" [81,81,81] 80) |
17 "rcoset_mult R I A B \<equiv> \<Union>a\<in>A. \<Union>b\<in>B. I +> (a \<otimes> b)" |
17 where "rcoset_mult R I A B \<equiv> \<Union>a\<in>A. \<Union>b\<in>B. I +>\<^bsub>R\<^esub> (a \<otimes>\<^bsub>R\<^esub> b)" |
18 |
18 |
19 |
19 |
20 text {* @{const "rcoset_mult"} fulfils the properties required by |
20 text {* @{const "rcoset_mult"} fulfils the properties required by |
21 congruences *} |
21 congruences *} |
22 lemma (in ideal) rcoset_mult_add: |
22 lemma (in ideal) rcoset_mult_add: |
87 qed |
87 qed |
88 |
88 |
89 |
89 |
90 subsection {* Quotient Ring Definition *} |
90 subsection {* Quotient Ring Definition *} |
91 |
91 |
92 constdefs (structure R) |
92 definition |
93 FactRing :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) ring" |
93 FactRing :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) ring" (infixl "Quot" 65) |
94 (infixl "Quot" 65) |
94 where "FactRing R I \<equiv> |
95 "FactRing R I \<equiv> |
95 \<lparr>carrier = a_rcosets\<^bsub>R\<^esub> I, mult = rcoset_mult R I, one = (I +>\<^bsub>R\<^esub> \<one>\<^bsub>R\<^esub>), zero = I, add = set_add R\<rparr>" |
96 \<lparr>carrier = a_rcosets I, mult = rcoset_mult R I, one = (I +> \<one>), zero = I, add = set_add R\<rparr>" |
|
97 |
96 |
98 |
97 |
99 subsection {* Factorization over General Ideals *} |
98 subsection {* Factorization over General Ideals *} |
100 |
99 |
101 text {* The quotient is a ring *} |
100 text {* The quotient is a ring *} |