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"