src/HOL/Algebra/QuotRing.thy
 changeset 35847 19f1f7066917 parent 29242 e190bc2a5399 child 35848 5443079512ea
equal inserted replaced
35846:2ae4b7585501 35847:19f1f7066917
`     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 *}`