# HG changeset patch # User paulson # 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]: "(\i\A. \) = \" +lemma finprod_one_eqI: "(\x. x \ A \ f x = \) \ finprod G f A = \" proof (induct A rule: infinite_finite_induct) case empty show ?case by simp next case (insert a A) - have "(%i. \) \ A \ carrier G" by auto + have "(\i. \) \ A \ carrier G" by auto with insert show ?case by simp qed simp +lemma finprod_one [simp]: "(\i\A. \) = \" + by (simp add: finprod_one_eqI) + lemma finprod_closed [simp]: fixes A assumes f: "f \ A \ 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 "\ = \" - apply (rule finprod_one) + apply (rule finprod_one_eqI) apply auto apply (subst finprod_insert) apply auto