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)"