src/HOL/Algebra/FiniteProduct.thy
 changeset 68447 0beb927eed89 parent 68445 c183a6a69f2d child 68458 023b353911c5
```     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Thu Jun 14 14:23:48 2018 +0100
1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Thu Jun 14 15:20:10 2018 +0100
1.3 @@ -332,15 +332,18 @@
1.4    apply (auto simp add: finprod_def)
1.5    done
1.6
1.7 -lemma finprod_one [simp]: "(\<Otimes>i\<in>A. \<one>) = \<one>"
1.8 +lemma finprod_one_eqI: "(\<And>x. x \<in> A \<Longrightarrow> f x = \<one>) \<Longrightarrow> finprod G f A = \<one>"
1.9  proof (induct A rule: infinite_finite_induct)
1.10    case empty show ?case by simp
1.11  next
1.12    case (insert a A)
1.13 -  have "(%i. \<one>) \<in> A \<rightarrow> carrier G" by auto
1.14 +  have "(\<lambda>i. \<one>) \<in> A \<rightarrow> carrier G" by auto
1.15    with insert show ?case by simp
1.16  qed simp
1.17
1.18 +lemma finprod_one [simp]: "(\<Otimes>i\<in>A. \<one>) = \<one>"
1.19 +  by (simp add: finprod_one_eqI)
1.20 +
1.21  lemma finprod_closed [simp]:
1.22    fixes A
1.23    assumes f: "f \<in> A \<rightarrow> carrier G"
```