author paulson Thu, 14 Jun 2018 15:20:10 +0100 changeset 68447 0beb927eed89 parent 68446 92ddca1edc43 child 68448 3d1517f3ba49
Adjusting Number_Theory for new Algebra
```--- 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" ```
```--- 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```