src/HOL/Algebra/FiniteProduct.thy
 changeset 68445 c183a6a69f2d parent 67613 ce654b0e6d69 child 68447 0beb927eed89
```     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Tue Jun 12 16:09:12 2018 +0100
1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Thu Jun 14 14:23:38 2018 +0100
1.3 @@ -524,4 +524,49 @@
1.4
1.5  end
1.6
1.7 +(* Jeremy Avigad. This should be generalized to arbitrary groups, not just commutative
1.8 +   ones, using Lagrange's theorem. *)
1.9 +
1.10 +lemma (in comm_group) power_order_eq_one:
1.11 +  assumes fin [simp]: "finite (carrier G)"
1.12 +    and a [simp]: "a \<in> carrier G"
1.13 +  shows "a [^] card(carrier G) = one G"
1.14 +proof -
1.15 +  have "(\<Otimes>x\<in>carrier G. x) = (\<Otimes>x\<in>carrier G. a \<otimes> x)"
1.16 +    by (subst (2) finprod_reindex [symmetric],
1.17 +      auto simp add: Pi_def inj_on_const_mult surj_const_mult)
1.18 +  also have "\<dots> = (\<Otimes>x\<in>carrier G. a) \<otimes> (\<Otimes>x\<in>carrier G. x)"
1.19 +    by (auto simp add: finprod_multf Pi_def)
1.20 +  also have "(\<Otimes>x\<in>carrier G. a) = a [^] card(carrier G)"
1.21 +    by (auto simp add: finprod_const)
1.22 +  finally show ?thesis
1.23 +(* uses the preceeding lemma *)
1.24 +    by auto
1.25 +qed
1.26 +
1.27 +
1.28 +lemma (in comm_monoid) finprod_UN_disjoint:
1.29 +  "finite I \<Longrightarrow> (\<forall>i\<in>I. finite (A i)) \<longrightarrow> (\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}) \<longrightarrow>
1.30 +    (\<forall>i\<in>I. \<forall>x \<in> A i. g x \<in> carrier G) \<longrightarrow>
1.31 +    finprod G g (UNION I A) = finprod G (\<lambda>i. finprod G g (A i)) I"
1.32 +  apply (induct set: finite)
1.33 +   apply force
1.34 +  apply clarsimp
1.35 +  apply (subst finprod_Un_disjoint)
1.36 +       apply blast
1.37 +      apply (erule finite_UN_I)
1.38 +      apply blast
1.39 +     apply (fastforce)
1.40 +    apply (auto intro!: funcsetI finprod_closed)
1.41 +  done
1.42 +
1.43 +lemma (in comm_monoid) finprod_Union_disjoint:
1.44 +  "finite C \<Longrightarrow>
1.45 +    \<forall>A\<in>C. finite A \<and> (\<forall>x\<in>A. f x \<in> carrier G) \<Longrightarrow>
1.46 +    \<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {} \<Longrightarrow>
1.47 +    finprod G f (\<Union>C) = finprod G (finprod G f) C"
1.48 +  apply (frule finprod_UN_disjoint [of C id f])
1.49 +  apply auto
1.50 +  done
1.51 +
1.52  end
```