equal
deleted
inserted
replaced
1 (* |
1 (* Title: HOL/Algebra/QuotRing.thy |
2 Title: HOL/Algebra/QuotRing.thy |
2 Author: Stephan Hohe |
3 Author: Stephan Hohe |
|
4 *) |
3 *) |
5 |
4 |
6 theory QuotRing |
5 theory QuotRing |
7 imports RingHom |
6 imports RingHom |
8 begin |
7 begin |
178 apply (rule quotient_is_cring) |
177 apply (rule quotient_is_cring) |
179 apply (rule is_cring) |
178 apply (rule is_cring) |
180 done |
179 done |
181 qed |
180 qed |
182 |
181 |
|
182 |
183 subsection {* Factorization over Prime Ideals *} |
183 subsection {* Factorization over Prime Ideals *} |
184 |
184 |
185 text {* The quotient ring generated by a prime ideal is a domain *} |
185 text {* The quotient ring generated by a prime ideal is a domain *} |
186 lemma (in primeideal) quotient_is_domain: |
186 lemma (in primeideal) quotient_is_domain: |
187 shows "domain (R Quot I)" |
187 shows "domain (R Quot I)" |