# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1528986010 -3600
# Node ID 0beb927eed8976af7b057313c93b2a63cbf50314
# Parent  92ddca1edc4394ae80188cd190b28d94f7742cde
Adjusting Number_Theory for new Algebra

diff -r 92ddca1edc43 -r 0beb927eed89 src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Thu Jun 14 14:23:48 2018 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy	Thu Jun 14 15:20:10 2018 +0100
@@ -332,15 +332,18 @@
   apply (auto simp add: finprod_def)
   done
 
-lemma finprod_one [simp]: "(\<Otimes>i\<in>A. \<one>) = \<one>"
+lemma finprod_one_eqI: "(\<And>x. x \<in> A \<Longrightarrow> f x = \<one>) \<Longrightarrow> finprod G f A = \<one>"
 proof (induct A rule: infinite_finite_induct)
   case empty show ?case by simp
 next
   case (insert a A)
-  have "(%i. \<one>) \<in> A \<rightarrow> carrier G" by auto
+  have "(\<lambda>i. \<one>) \<in> A \<rightarrow> carrier G" by auto
   with insert show ?case by simp
 qed simp
 
+lemma finprod_one [simp]: "(\<Otimes>i\<in>A. \<one>) = \<one>"
+  by (simp add: finprod_one_eqI)
+
 lemma finprod_closed [simp]:
   fixes A
   assumes f: "f \<in> A \<rightarrow> carrier G" 
diff -r 92ddca1edc43 -r 0beb927eed89 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Thu Jun 14 14:23:48 2018 +0100
+++ b/src/HOL/Number_Theory/Residues.thy	Thu Jun 14 15:20:10 2018 +0100
@@ -10,9 +10,6 @@
 theory Residues
 imports
   Cong
-  "HOL-Algebra.More_Group"
-  "HOL-Algebra.More_Ring"
-  "HOL-Algebra.More_Finite_Product"
   "HOL-Algebra.Multiplicative_Group"
   Totient
 begin
@@ -355,7 +352,7 @@
      apply (metis Units_inv_inv)+
     done
   also have "\<dots> = \<one>"
-    apply (rule finprod_one)
+    apply (rule finprod_one_eqI)
      apply auto
     apply (subst finprod_insert)
         apply auto