src/HOL/Algebra/QuotRing.thy
 changeset 68583 654e73d05495 parent 68551 b680e74eb6f2 child 68584 ec4fe1032b6e
```     1.1 --- a/src/HOL/Algebra/QuotRing.thy	Tue Jul 03 00:15:16 2018 +0100
1.2 +++ b/src/HOL/Algebra/QuotRing.thy	Tue Jul 03 10:07:24 2018 +0100
1.3 @@ -1022,6 +1022,18 @@
1.4    shows "R Quot (a_kernel R S h) \<simeq> S"
1.5    using FactRing_iso_set assms is_ring_iso_def by auto
1.6
1.7 +corollary (in ring) FactRing_zeroideal:
1.8 +  shows "R Quot { \<zero> } \<simeq> R" and "R \<simeq> R Quot { \<zero> }"
1.9 +proof -
1.10 +  have "ring_hom_ring R R id"
1.11 +    using ring_axioms by (auto intro: ring_hom_ringI)
1.12 +  moreover have "a_kernel R R id = { \<zero> }"
1.13 +    unfolding a_kernel_def' by auto
1.14 +  ultimately show "R Quot { \<zero> } \<simeq> R" and "R \<simeq> R Quot { \<zero> }"
1.15 +    using ring_hom_ring.FactRing_iso[of R R id]
1.16 +          ring_iso_sym[OF ideal.quotient_is_ring[OF zeroideal], of R] by auto
1.17 +qed
1.18 +
1.19  lemma (in ring_hom_ring) img_is_ring: "ring (S \<lparr> carrier := h ` (carrier R) \<rparr>)"
1.20  proof -
1.21    let ?the_elem = "\<lambda>X. the_elem (h ` X)"
```