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