--- a/src/HOL/Algebra/Algebra.thy Thu Apr 04 23:05:53 2019 +0200
+++ b/src/HOL/Algebra/Algebra.thy Fri Apr 05 11:22:00 2019 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/Algebra/Algebra.thy *)
theory Algebra
- imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Product_Groups
+ imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Free_Abelian_Groups
Divisibility Embedded_Algebras IntRing Sym_Groups Exact_Sequence Polynomials
begin
end
--- a/src/HOL/Algebra/Free_Abelian_Groups.thy Thu Apr 04 23:05:53 2019 +0200
+++ b/src/HOL/Algebra/Free_Abelian_Groups.thy Fri Apr 05 11:22:00 2019 +0100
@@ -2,7 +2,7 @@
theory Free_Abelian_Groups
imports
- Product_Groups "HOL-Cardinals.Cardinal_Arithmetic"
+ Product_Groups "../Cardinals/Cardinal_Arithmetic"
"HOL-Library.Countable_Set" "HOL-Library.Poly_Mapping" "HOL-Library.Equipollence"
begin
@@ -594,7 +594,6 @@
by (auto simp: hom_def free_Abelian_group_def Pi_def)
qed
-
proposition iso_free_Abelian_group_sum:
assumes "pairwise (\<lambda>i j. disjnt (S i) (S j)) I"
shows "(\<lambda>f. sum' f I) \<in> iso (sum_group I (\<lambda>i. free_Abelian_group(S i))) (free_Abelian_group (\<Union>(S ` I)))"
@@ -610,8 +609,7 @@
done
show "?h (x \<otimes>\<^bsub>?G\<^esub> y) = ?h x \<otimes>\<^bsub>?H\<^esub> ?h y"
if "x \<in> carrier ?G" "y \<in> carrier ?G" for x y
- using that apply (simp add: sum.finite_Collect_op carrier_sum_group sum.distrib')
- sorry
+ using that by (simp add: sum.finite_Collect_op carrier_sum_group sum.distrib')
qed
interpret GH: group_hom "?G" "?H" "?h"
using hom by (simp add: group_hom_def group_hom_axioms_def)
--- a/src/HOL/Library/FuncSet.thy Thu Apr 04 23:05:53 2019 +0200
+++ b/src/HOL/Library/FuncSet.thy Fri Apr 05 11:22:00 2019 +0100
@@ -220,6 +220,12 @@
lemma restrict_Pi_cancel: "restrict x I \<in> Pi I A \<longleftrightarrow> x \<in> Pi I A"
by (auto simp: restrict_def Pi_def)
+lemma sum_restrict' [simp]: "sum' (\<lambda>i\<in>I. g i) I = sum' (\<lambda>i. g i) I"
+ by (simp add: sum.G_def conj_commute cong: conj_cong)
+
+lemma prod_restrict' [simp]: "prod' (\<lambda>i\<in>I. g i) I = prod' (\<lambda>i. g i) I"
+ by (simp add: prod.G_def conj_commute cong: conj_cong)
+
subsection \<open>Bijections Between Sets\<close>