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