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