# HG changeset patch
# User paulson
# Date 1530608855 -3600
# Node ID ec4fe1032b6e03205a7a6ad1a9c7027388486d22
# Parent  b9b9e29858782ba21c31d49417b9a7fc86da064a# Parent  654e73d05495c2f39b25ea2491c4dd9f977899d1
merged

diff -r b9b9e2985878 -r ec4fe1032b6e src/HOL/Algebra/Multiplicative_Group.thy
--- a/src/HOL/Algebra/Multiplicative_Group.thy	Tue Jul 03 11:00:37 2018 +0200
+++ b/src/HOL/Algebra/Multiplicative_Group.thy	Tue Jul 03 10:07:35 2018 +0100
@@ -609,16 +609,16 @@
 definition mult_of :: "('a, 'b) ring_scheme \<Rightarrow> 'a monoid" where
   "mult_of R \<equiv> \<lparr> carrier = carrier R - {\<zero>\<^bsub>R\<^esub>}, mult = mult R, one = \<one>\<^bsub>R\<^esub>\<rparr>"
 
-lemma carrier_mult_of: "carrier (mult_of R) = carrier R - {\<zero>\<^bsub>R\<^esub>}"
+lemma carrier_mult_of [simp]: "carrier (mult_of R) = carrier R - {\<zero>\<^bsub>R\<^esub>}"
   by (simp add: mult_of_def)
 
-lemma mult_mult_of: "mult (mult_of R) = mult R"
+lemma mult_mult_of [simp]: "mult (mult_of R) = mult R"
  by (simp add: mult_of_def)
 
 lemma nat_pow_mult_of: "([^]\<^bsub>mult_of R\<^esub>) = (([^]\<^bsub>R\<^esub>) :: _ \<Rightarrow> nat \<Rightarrow> _)"
   by (simp add: mult_of_def fun_eq_iff nat_pow_def)
 
-lemma one_mult_of: "\<one>\<^bsub>mult_of R\<^esub> = \<one>\<^bsub>R\<^esub>"
+lemma one_mult_of [simp]: "\<one>\<^bsub>mult_of R\<^esub> = \<one>\<^bsub>R\<^esub>"
   by (simp add: mult_of_def)
 
 lemmas mult_of_simps = carrier_mult_of mult_mult_of nat_pow_mult_of one_mult_of
diff -r b9b9e2985878 -r ec4fe1032b6e src/HOL/Algebra/Polynomials.thy
diff -r b9b9e2985878 -r ec4fe1032b6e src/HOL/Algebra/QuotRing.thy
--- a/src/HOL/Algebra/QuotRing.thy	Tue Jul 03 11:00:37 2018 +0200
+++ b/src/HOL/Algebra/QuotRing.thy	Tue Jul 03 10:07:35 2018 +0100
@@ -1021,6 +1021,18 @@
   shows "R Quot (a_kernel R S h) \<simeq> S"
   using FactRing_iso_set assms is_ring_iso_def by auto
 
+corollary (in ring) FactRing_zeroideal:
+  shows "R Quot { \<zero> } \<simeq> R" and "R \<simeq> R Quot { \<zero> }"
+proof -
+  have "ring_hom_ring R R id"
+    using ring_axioms by (auto intro: ring_hom_ringI)
+  moreover have "a_kernel R R id = { \<zero> }"
+    unfolding a_kernel_def' by auto
+  ultimately show "R Quot { \<zero> } \<simeq> R" and "R \<simeq> R Quot { \<zero> }"
+    using ring_hom_ring.FactRing_iso[of R R id]
+          ring_iso_sym[OF ideal.quotient_is_ring[OF zeroideal], of R] by auto
+qed
+
 lemma (in ring_hom_ring) img_is_ring: "ring (S \<lparr> carrier := h ` (carrier R) \<rparr>)"
 proof -
   let ?the_elem = "\<lambda>X. the_elem (h ` X)"
diff -r b9b9e2985878 -r ec4fe1032b6e src/HOL/Algebra/Ring_Divisibility.thy