diff --git a/thys/Dirichlet_L/Group_Adjoin.thy b/thys/Dirichlet_L/Group_Adjoin.thy
deleted file mode 100644
--- a/thys/Dirichlet_L/Group_Adjoin.thy
+++ /dev/null
@@ -1,504 +0,0 @@
- (*
-    File:      Group_Adjoin.thy
-    Author:    Manuel Eberl, TU München
-*)
-section \<open>Adjoining Elements to a Finite Abelian Group\<close>
-theory Group_Adjoin
-imports 
-  Complex_Main
-  "HOL-Algebra.Multiplicative_Group"
-begin
-
-text \<open>
-  This theory provides the notion of adjoining a single element to a subgroup of a finite
-  abelian group, and, in particular, an induction principle based upon this: We can show that
-  some property holds for a group by showing that it holds for some fixed subgroup and that
-  it is preserved when adjoining a single element.
-
-  The general idea for this was taken from Apostol's 
-  ``Analytic Number Theory''~\cite{apostol1976analytic}.
-\<close>
-
-subsection \<open>Miscellaneous Group Theory\<close>
-
-lemma (in group) ord_min:
-  assumes "m \<ge> 1" "x \<in> carrier G" "x [^] m = \<one>"
-  shows   "ord x \<le> m"
-  using assms pow_eq_id by auto
-
-lemma (in group) bij_betw_mult_left [intro]:
-  assumes [simp]: "x \<in> carrier G"
-  shows "bij_betw (\<lambda>y. x \<otimes> y) (carrier G) (carrier G)"
-  by (intro bij_betwI[where ?g = "\<lambda>y. inv x \<otimes> y"])
-     (auto simp: m_assoc [symmetric])
-
-locale finite_comm_group = comm_group +
-  assumes fin [intro]: "finite (carrier G)"
-begin
-
-lemma order_gt_0 [simp,intro]: "order G > 0"
-  by (subst order_gt_0_iff_finite) auto
-
-lemma subgroup_imp_finite_comm_group:
-  assumes "subgroup H G"
-  shows   "finite_comm_group (G\<lparr>carrier := H\<rparr>)"
-proof -
-  interpret G': group "G\<lparr>carrier := H\<rparr>" by (intro subgroup_imp_group) fact+
-  interpret H: subgroup H G by fact
-  show ?thesis by standard (insert finite_subset[OF H.subset fin], auto simp: m_comm)
-qed
-
-end
-
-
-subsection \<open>Subgroup indicators and adjoining elements\<close>
-
-definition subgroup_indicator :: "('a, 'b) monoid_scheme \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> nat" where
-  "subgroup_indicator G H a = (LEAST k. k > 0 \<and> a [^]\<^bsub>G\<^esub> k \<in> H)"
-
-definition adjoin :: "('a, 'b) monoid_scheme \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'a set" where
-  "adjoin G H a = {x \<otimes>\<^bsub>G\<^esub> a [^]\<^bsub>G\<^esub> k |x k. x \<in> H \<and> k < subgroup_indicator G H a}"
-
-lemma (in subgroup) nat_pow_closed [simp,intro]: "a \<in> H \<Longrightarrow> pow G a (n::nat) \<in> H"
-  by (induction n) (auto simp: nat_pow_def)
-
-lemma nat_pow_modify_carrier: "a [^]\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> b = a [^]\<^bsub>G\<^esub> (b::nat)"
-  by (simp add: nat_pow_def)
-
-lemma subgroup_indicator_modify_carrier [simp]:
-  "subgroup_indicator (G\<lparr>carrier := H'\<rparr>) H a = subgroup_indicator G H a"
-  by (auto simp: subgroup_indicator_def nat_pow_def)
-
-lemma adjoin_modify_carrier [simp]:
-  "adjoin (G\<lparr>carrier := H'\<rparr>) H a = adjoin G H a"
-  by (simp_all add: adjoin_def nat_pow_def)
-
-context group
-begin
-
-lemma subgroup_indicator_eq_1:
-  assumes "a \<in> H" "a \<in> carrier G"
-  shows   "subgroup_indicator G H a = 1"
-proof -
-  from assms show ?thesis
-    unfolding subgroup_indicator_def
-    by (intro Least_equality) (auto simp: nat_pow_def)
-qed
-
-lemma subgroup_indicator_le:
-  assumes "a [^] n \<in> H" "n > 0"  "a \<in> carrier G"
-  shows   "subgroup_indicator G H a \<le> n"
-  using assms unfolding subgroup_indicator_def by (intro Least_le) auto
-
-end
-
-context finite_comm_group
-begin
-
-lemma ord_pos: 
-  assumes "x \<in> carrier G"
-  shows   "ord x > 0"
-  using ord_ge_1[of x] assms fin by auto
-
-lemma 
-  assumes "subgroup H G" and a: "a \<in> carrier G"
-  shows subgroup_indicator_pos: "subgroup_indicator G H a > 0" (is "?h > 0")
-  and   pow_subgroup_indicator: "a [^] subgroup_indicator G H a \<in> H"
-proof -
-  interpret subgroup H G by fact
-  from a have "\<exists>h>0. a [^] (h::nat) \<in> H"
-    by (intro exI[of _ "ord a"]) (auto simp: ord_pos pow_ord_eq_1 fin)
-  hence "?h > 0 \<and> a [^] ?h \<in> H" unfolding subgroup_indicator_def
-    by (rule LeastI_ex)
-  thus "?h > 0" and "a [^] ?h \<in> H" by auto
-qed
-
-lemma subgroup_indicator_le_ord:
-  assumes "a \<in> carrier G" "subgroup H G"
-  shows   "subgroup_indicator G H a \<le> ord a"
-proof -
-  interpret subgroup H G by fact
-  from assms show ?thesis by (intro subgroup_indicator_le) (auto simp: pow_ord_eq_1 fin ord_pos)
-qed
-
-lemma subgroup_indicator_trivial: 
-  assumes "a \<in> carrier G"
-  shows   "subgroup_indicator G {\<one>} a = group.ord G a"
-proof -
-  have sg[simp]: "subgroup {\<one>} G" by standard auto
-  from pow_subgroup_indicator[OF sg assms] and assms show ?thesis
-    by (intro antisym subgroup_indicator_le_ord ord_min)
-       (auto simp: Suc_le_eq subgroup_indicator_pos)
-qed
-
-lemma mem_adjoin:
-  assumes "subgroup H G" "x \<in> H" "a \<in> carrier G"
-  shows   "x \<in> adjoin G H a"
-proof -
-  interpret subgroup H G by fact
-  from assms show ?thesis
-    by (auto simp: adjoin_def intro!: exI[of _ x] exI[of _ 0] subgroup_indicator_pos)
-qed
-
-lemma adjoin_subgroup:
-  assumes "subgroup H G" and a: "a \<in> carrier G"
-  shows   "subgroup (adjoin G H a) G"
-proof (standard, goal_cases)
-  case 1
-  interpret subgroup H G by fact
-  from a show ?case by (auto simp: adjoin_def)
-next
-  case (2 x y)
-  interpret subgroup H G by fact
-  define h where "h = subgroup_indicator G H a"
-  from assms have [simp]: "h > 0" 
-    unfolding h_def by (intro subgroup_indicator_pos) auto
-  from 2(1) obtain x' :: 'a and k :: nat where [simp]: "x' \<in> H" "x = x' \<otimes> a [^] k"
-    by (auto simp: adjoin_def)
-  from 2(2) obtain y' :: 'a and l :: nat where [simp]: "y' \<in> H" "y = y' \<otimes> a [^] l"
-    by (auto simp: adjoin_def)
-  define a' where "a' = (a [^] h) [^] ((k + l) div h)"
-  have [simp]: "a' \<in> H" unfolding a'_def
-    by (rule nat_pow_closed) (insert assms, auto simp: h_def intro!: pow_subgroup_indicator)
-  from a have "x \<otimes> y = (x' \<otimes> y') \<otimes> a [^] (k + l)"
-    by (simp add: nat_pow_mult [symmetric] m_ac)
-  also have "k + l = h * ((k + l) div h) + (k + l) mod h"
-    by (rule mult_div_mod_eq [symmetric])
-  also from a fin have "a [^] \<dots> = a' \<otimes> a [^] ((k + l) mod h)"
-    by (subst nat_pow_mult [symmetric]) 
-       (simp_all add: nat_pow_pow [symmetric] pow_ord_eq_1 a'_def [symmetric])
-  finally have "x \<otimes> y = x' \<otimes> y' \<otimes> a' \<otimes> a [^] ((k + l) mod h)" 
-    using a by (simp add: m_ac)
-  moreover from a have "(k + l) mod h < h"
-    by (intro mod_less_divisor) (auto simp: ord_pos)
-  ultimately show ?case
-    by (auto simp: adjoin_def h_def intro!: exI[of _ "x' \<otimes> y' \<otimes> a'"] exI[of _ "(k + l) mod h"])
-next
-  case 3
-  interpret subgroup H G by fact
-  from assms show ?case
-    by (auto simp: adjoin_def intro!: exI[of _ \<one>] exI[of _ 0] subgroup_indicator_pos)
-next
-  case (4 x)
-  interpret H: subgroup H G by fact
-  define h where "h = subgroup_indicator G H a"
-  define a' where "a' = a [^] h"
-  from assms have [simp]: "a' \<in> H" unfolding a'_def h_def
-    by (intro pow_subgroup_indicator) auto
-  from 4 obtain x' and k :: nat where [simp]: "x' \<in> H" "x = x' \<otimes> a [^] k" and "k < h"
-    by (auto simp: adjoin_def h_def)
-  show ?case
-  proof (cases "k = 0")
-    case True
-    with assms show ?thesis
-      by (auto simp: mem_adjoin)
-  next
-    case False
-    from a have "inv x = inv x' \<otimes> inv (a [^] k)"
-      by (simp add: inv_mult)
-    also have "\<dots> = inv x' \<otimes> (inv a' \<otimes> a') \<otimes> inv (a [^] k)" by simp
-    also have "\<dots> = inv x' \<otimes> inv a' \<otimes> (a' \<otimes> inv (a [^] k))"
-      by (simp only: \<open>a' \<in> H\<close> \<open>x' \<in> H\<close> inv_closed m_closed H.mem_carrier m_ac nat_pow_closed a)
-    also from a have "a' \<otimes> inv (a [^] k) = a [^] (int h - int k)"
-      by (subst int_pow_diff) (auto simp: a'_def int_pow_int)
-    also from \<open>k < h\<close> have "int h - int k = int (h - k)"
-      by simp
-    also have "a [^] \<dots> = a [^] (h - k)" 
-      by (simp add: int_pow_int)
-    finally have "inv x = inv x' \<otimes> inv a' \<otimes> a [^] (h - k)" .
-    moreover have "h - k < h" using \<open>k < h\<close> and False by simp
-    ultimately show ?thesis
-      by (auto simp: adjoin_def h_def intro!: exI[of _ "inv x' \<otimes> inv a'"] exI[of _ "h - k"])
-  qed
-qed
-
-lemma adjoin_id:
-  assumes "subgroup H G" and a: "a \<in> H"
-  shows   "adjoin G H a = H"
-proof -
-  interpret subgroup H G by fact
-  show ?thesis
-  proof safe
-    fix x assume "x \<in> H"
-    with assms show "x \<in> adjoin G H a"
-      by (auto simp: adjoin_def intro!: exI[of _ x] exI[of _ 0] subgroup_indicator_pos)
-  qed (insert a, auto simp: adjoin_def)
-qed
-
-lemma adjoined_in_adjoin:
-  assumes "subgroup H G" and a: "a \<in> carrier G"
-  shows   "a \<in> adjoin G H a"
-proof (cases "a \<in> H")
-  case True
-  with assms show ?thesis by (subst adjoin_id) auto
-next
-  case False
-  interpret subgroup H G by fact
-  from assms have "subgroup_indicator G H a > 0" 
-    by (intro subgroup_indicator_pos) auto
-  moreover from False and assms and pow_subgroup_indicator[OF assms] 
-    have "subgroup_indicator G H a \<noteq> 1" by (intro notI) auto
-  ultimately have "subgroup_indicator G H a > 1" by simp
-  with assms show ?thesis
-    by (auto simp: adjoin_def intro!: exI[of _ \<one>] exI[of _ 1])
-qed
-
-lemma adjoin_subset:
-  assumes "subgroup H G" and a: "a \<in> carrier G"
-  shows   "adjoin G H a \<subseteq> carrier G"
-proof -
-  interpret subgroup H G by fact
-  from a show ?thesis by (auto simp: adjoin_def)
-qed
-
-lemma inj_on_adjoin:
-  assumes "subgroup H G" and a: "a \<in> carrier G" "a \<notin> H"
-  defines "h \<equiv> subgroup_indicator G H a"
-  shows   "inj_on (\<lambda>(x, k). x \<otimes> a [^] k) (H \<times> {..<h})"
-proof (intro inj_onI, clarify, goal_cases)
-  case (1 x k y l)
-  interpret H: subgroup H G by fact
-  have wf: "x \<in> carrier G" "y \<in> carrier G" "a [^] k \<in> carrier G" "a [^] l \<in> carrier G"
-    using 1 a by auto
-  have "x \<otimes> inv y = (x \<otimes> inv y) \<otimes> (a [^] k \<otimes> inv (a [^] k))"
-    by (simp add: wf)
-  also have "\<dots> = x \<otimes> a [^] k \<otimes> inv y \<otimes> inv (a [^] k)"
-    by (simp only: m_ac wf inv_closed m_closed)
-  also from a have "\<dots> = y \<otimes> a [^] l \<otimes> inv y \<otimes> inv (a [^] k)"
-    by (subst 1) (simp_all)
-  also have "\<dots> = y \<otimes> inv y \<otimes> (a [^] l \<otimes> inv (a [^] k))"
-    by (simp only: m_ac wf inv_closed m_closed)
-  also from wf have "\<dots> = a [^] int l \<otimes> inv (a [^] int k)"
-    by (simp add: int_pow_int)
-  also have "\<dots> = a [^] (int l - int k)"
-    by (rule int_pow_diff [symmetric]) fact+
-  finally have *: "x \<otimes> inv y = a [^] (int l - int k)" .
-
-  have **: "a [^] (nat \<bar>int l - int k\<bar>) \<in> H"
-  proof (cases "k \<le> l")
-    case True
-    from 1 have "a [^] (int l - int k) \<in> H" by (subst * [symmetric]) auto
-    also have "a [^] (int l - int k) = a [^] (nat \<bar>int l - int k\<bar>)"
-      using True by (simp add: nat_diff_distrib int_pow_int [symmetric] of_nat_diff)
-    finally show ?thesis .
-  next
-    case False
-    from 1 have "inv (a [^] (int l - int k)) \<in> H" by (subst * [symmetric]) auto
-    also have "inv (a [^] (int l - int k)) = a [^] (nat \<bar>int l - int k\<bar>)" using False a 
-      by (simp add: int_pow_neg [symmetric] nat_diff_distrib int_pow_int [symmetric] of_nat_diff)
-    finally show ?thesis .
-  qed
-  have "k = l"
-  proof (rule ccontr)
-    assume "k \<noteq> l"
-    with a and ** have "h \<le> nat \<bar>int l - int k\<bar>" unfolding h_def
-      by (intro subgroup_indicator_le) auto
-    also have "\<dots> < h" using \<open>l < h\<close> and \<open>k < h\<close> by linarith
-    finally show False ..
-  qed
-  with 1 and a show ?case by simp
-qed
-
-lemma card_adjoin:
-  assumes "subgroup H G" and a: "a \<in> carrier G" "a \<notin> H"
-  shows   "card (adjoin G H a) = card H * subgroup_indicator G H a"
-proof -
-  interpret H: subgroup H G by fact
-  define h where "h = subgroup_indicator G H a"
-  have "adjoin G H a = (\<lambda>(x,k). x \<otimes> a [^] k) ` (H \<times> {..<h})"
-    by (auto simp: adjoin_def h_def)
-  also have "card \<dots> = card (H \<times> {..<h})" unfolding h_def
-    by (intro card_image inj_on_adjoin assms)
-  finally show ?thesis by (simp add: h_def card_cartesian_product)
-qed
-
-end
-
-locale finite_comm_group_adjoin = finite_comm_group + subgroup H
-  for H +
-  fixes a :: 'a
-  assumes a_in_carrier [simp]: "a \<in> carrier G"
-  assumes a_notin_subgroup: "a \<notin> H"
-begin
-
-definition unadjoin :: "'a \<Rightarrow> 'a \<times> nat"  where
-  "unadjoin x = 
-     (THE z. z \<in> H \<times> {..<subgroup_indicator G H a} \<and> x = fst z \<otimes>\<^bsub>G\<^esub> a [^]\<^bsub>G\<^esub> snd z)"
-
-lemma adjoin_unique:
-  assumes "x \<in> adjoin G H a"
-  defines "h \<equiv> subgroup_indicator G H a"
-  shows   "\<exists>!z. z \<in> H \<times> {..<subgroup_indicator G H a} \<and> x = fst z \<otimes>\<^bsub>G\<^esub> a [^]\<^bsub>G\<^esub> snd z"
-proof (rule ex_ex1I, goal_cases)
-  case 1
-  from assms show ?case by (auto simp: adjoin_def)
-next
-  case (2 z1 z2)
-  have "subgroup H G" ..
-  from inj_on_adjoin[OF this a_in_carrier a_notin_subgroup]
-  show ?case by (rule inj_onD) (use 2 in auto)
-qed
-
-lemma unadjoin_correct:
-  assumes "x \<in> adjoin G H a"
-  shows   "fst (unadjoin x) \<in> H" and "snd (unadjoin x) < subgroup_indicator G H a"
-          "fst (unadjoin x) \<otimes> a [^] snd (unadjoin x) = x"
-  using theI'[OF adjoin_unique[OF assms], folded unadjoin_def] by auto
-
-lemma unadjoin_unique:
-  assumes "y \<in> H" "h < subgroup_indicator G H a"
-  shows   "unadjoin (y \<otimes> a [^] h) = (y, h)"
-proof -
-  from assms have "y \<otimes> a [^] h \<in> adjoin G H a" by (auto simp: adjoin_def)
-  note * = theI'[OF adjoin_unique[OF this], folded unadjoin_def]
-  from inj_on_adjoin[OF is_subgroup a_in_carrier a_notin_subgroup] show ?thesis
-    by (rule inj_onD) (insert * assms, auto)
-qed
-
-lemma unadjoin_unique':
-  assumes "y \<in> H" "h < subgroup_indicator G H a" "x = y \<otimes> a [^] h"
-  shows   "unadjoin x = (y, h)"
-  using unadjoin_unique[OF assms(1,2)] assms(3) by simp
-
-lemma unadjoin_1 [simp]: "unadjoin \<one> = (\<one>, 0)"
-  by (intro unadjoin_unique') (auto intro!: subgroup_indicator_pos is_subgroup)
-
-lemma unadjoin_in_base [simp]: "x \<in> H \<Longrightarrow> unadjoin x = (x, 0)"
-  by (intro unadjoin_unique') (auto intro!: subgroup_indicator_pos is_subgroup)
-
-lemma unadjoin_adjoined [simp]: "unadjoin a = (\<one>, 1)"
-proof (rule unadjoin_unique')
-  have "subgroup_indicator G H a \<noteq> 1" using is_subgroup a_notin_subgroup
-    using pow_subgroup_indicator[of H a] by auto
-  with subgroup_indicator_pos [OF is_subgroup a_in_carrier] 
-    show "subgroup_indicator G H a > 1" by simp
-qed auto
-
-end
-
-
-subsection \<open>Induction by adjoining elements\<close>
-
-context finite_comm_group
-begin
-
-lemma group_decompose_adjoin_aux:
-  assumes "subgroup H G"
-  shows   "H = carrier G \<or> 
-           (\<exists>H' a. H \<subseteq> H' \<and> subgroup H' G \<and> a \<in> carrier G - H' \<and> carrier G = adjoin G H' a)"
-proof -
-  have ind: "(\<And>H. subgroup H G \<Longrightarrow> H \<noteq> carrier G \<Longrightarrow> P (adjoin G H (SOME a. a \<in> carrier G - H))
-                \<Longrightarrow> P H) \<Longrightarrow> (\<And>H. subgroup H G \<Longrightarrow> H = carrier G \<Longrightarrow> P H) \<Longrightarrow>
-                (\<And>H. \<not> subgroup H G \<Longrightarrow> P H) \<Longrightarrow> P a0" for P a0
-  proof (induction_schema, force, rule wf_bounded_set)
-    fix H assume H: "subgroup H G" "H \<noteq> carrier G"
-    interpret subgroup H G by fact
-    from H have H': "H \<subset> carrier G" by auto
-    define a where "a = (SOME a. a \<in> carrier G - H)"
-    have a: "a \<in> carrier G - H" unfolding a_def
-      by (rule someI_ex) (insert H', auto)  
-    from a and H have "adjoin G H a \<subseteq> carrier G" by (intro adjoin_subset) auto
-    from a and H have "a \<in> adjoin G H a" "a \<notin> H"
-      by (auto simp: adjoined_in_adjoin)
-    hence "adjoin G H a \<noteq> H" by blast
-    with H and a show "(adjoin G H a, H) \<in> {(B,A). A \<subset> B \<and> B \<subseteq> carrier G}"
-      using adjoin_subset[of H a] by (auto intro: mem_adjoin)
-  next
-    fix A B assume "(B, A) \<in> {(B, A). A \<subset> B \<and> B \<subseteq> carrier G}"
-    thus "finite (carrier G) \<and> carrier G \<subseteq> carrier G \<and> B \<subseteq> carrier G \<and> A \<subset> B"
-      by auto
-  qed
-
-  from assms show ?thesis
-  proof (induction H rule: ind)
-    case (1 H)
-    interpret subgroup H G by fact
-    define a where "a = (SOME a. a \<in> carrier G - H)"
-    from "1.hyps" have "\<exists>a. a \<in> carrier G - H" by auto
-    hence a: "a \<in> carrier G - H" unfolding a_def by (rule someI_ex)
-  
-    from "1.hyps" and a have "subgroup (adjoin G H a) G"
-      by (intro adjoin_subgroup) auto
-    from "1.IH"[folded a_def, OF this] 
-      have "(\<exists>H' a. H \<subseteq> H' \<and> subgroup H' G \<and> a \<in> carrier G - H' \<and> carrier G = adjoin G H' a)"
-    proof (elim disjE, goal_cases)
-      case 1
-      with a and \<open>subgroup H G\<close> show ?case
-        by (intro exI[of _ H] exI[of _ a]) simp_all
-    next
-      case 2
-      then obtain H' a' where *: "adjoin G H a \<subseteq> H'" "subgroup H' G" 
-                                 "a' \<in> carrier G - H'" "carrier G = adjoin G H' a'" by blast
-      thus ?case using mem_adjoin[OF \<open>subgroup H G\<close>, of _ a] a
-        by (intro exI[of _ H'] exI[of _ a']) auto
-    qed
-    thus ?case by blast
-  qed auto
-qed
-
-lemma group_decompose_adjoin:
-  assumes "subgroup H0 G" "H0 \<noteq> carrier G"
-  obtains H a where "H0 \<subseteq> H" "subgroup H G" "a \<in> carrier G - H" "carrier G = adjoin G H a"
-proof -
-  from group_decompose_adjoin_aux[OF assms(1)] and assms(2) and that show ?thesis by blast
-qed
-
-lemma subgroup_adjoin_induct [consumes 1, case_names base adjoin]:
-  assumes "subgroup H0 G"
-  assumes base: "P (G\<lparr>carrier := H0\<rparr>)"
-  assumes adjoin: "\<And>H a. subgroup H G \<Longrightarrow> H0 \<subseteq> H \<Longrightarrow> a \<in> carrier G - H \<Longrightarrow> P (G\<lparr>carrier := H\<rparr>) \<Longrightarrow> 
-                           P (G\<lparr>carrier := adjoin G H a\<rparr>)"
-  shows   "P G"
-proof -
-  define H where "H = carrier G"
-  have "finite H" by (auto simp: H_def fin)
-  moreover have "subgroup H G" unfolding H_def by standard auto
-  moreover {
-    interpret subgroup H0 G by fact
-    have "H0 \<subseteq> H" by (simp add: H_def subset)
-  }
-  ultimately have "P (G\<lparr>carrier := H\<rparr>)"
-  proof (induction H rule: finite_psubset_induct)
-    case (psubset H)
-    show ?case
-    proof (cases "H = H0")
-      case True
-      thus ?thesis by (simp add: base)
-    next
-      case False
-      interpret H_sg: subgroup H G by fact
-      interpret H: finite_comm_group "G\<lparr>carrier := H\<rparr>"
-        by (rule subgroup_imp_finite_comm_group) fact
-      have sg: "subgroup H0 (G\<lparr>carrier := H\<rparr>)"
-        by (simp add: H_sg.subgroup_axioms \<open>subgroup H0 G\<close> psubset.prems(2) subgroup_incl)
-      from H.group_decompose_adjoin[OF sg] and False
-        obtain H' a where H': "H0 \<subseteq> H'" "subgroup H' (G\<lparr>carrier := H\<rparr>)" "a \<in> H - H'" 
-                              "H = adjoin G H' a" by (auto simp: order_def)
-      have "subgroup H' G"
-        using \<open>subgroup H G\<close> and H'(2) group.incl_subgroup by blast
-      from H' and adjoined_in_adjoin[of H' a] and \<open>subgroup H' G\<close> and mem_adjoin[of H' _ a]
-        have "a \<in> H" and "a \<notin> H'" and "H' \<subseteq> H" by auto
-      hence "H' \<subset> H" by blast
-      from psubset.IH [OF \<open>H' \<subset> H\<close> \<open>subgroup H' G\<close> \<open>H0 \<subseteq> H'\<close>] have "P (G\<lparr>carrier := H'\<rparr>)" .
-      with H' and \<open>subgroup H' G\<close> have "P (G\<lparr>carrier := adjoin G H' a\<rparr>)"
-        by (intro adjoin) auto
-      also from H' have "adjoin G H' a = H" by simp
-      finally show ?thesis .
-    qed
-  qed
-  thus "P G" by (simp add: H_def)
-qed
-
-lemma subgroup_adjoin_induct' [case_names singleton adjoin]:
-  assumes singleton: "P (G\<lparr>carrier := {\<one>}\<rparr>)"
-  assumes adjoin: "\<And>H a. subgroup H G \<Longrightarrow> a \<in> carrier G - H \<Longrightarrow> P (G\<lparr>carrier := H\<rparr>) \<Longrightarrow> 
-                           P (G\<lparr>carrier := adjoin G H a\<rparr>)"
-  shows   "P G"
-proof -
-  have "subgroup {\<one>} G" by standard auto
-  from this and assms show ?thesis by (rule subgroup_adjoin_induct)
-qed
-
-end
-
-end
\ No newline at end of file
diff --git a/thys/Dirichlet_L/Multiplicative_Characters.thy b/thys/Dirichlet_L/Multiplicative_Characters.thy
--- a/thys/Dirichlet_L/Multiplicative_Characters.thy
+++ b/thys/Dirichlet_L/Multiplicative_Characters.thy
@@ -1,896 +1,1667 @@
 (*
     File:      Multiplicative_Characters.thy
-    Author:    Manuel Eberl, TU München
+    Author:    Manuel Eberl, TU München; Joseph Thommes, TU München
 *)
 section \<open>Multiplicative Characters of Finite Abelian Groups\<close>
 theory Multiplicative_Characters
-imports
+  imports
   Complex_Main
-  Group_Adjoin
+  "Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups"
 begin
 
+notation integer_mod_group ("Z")
+
 subsection \<open>Definition of characters\<close>
 
 text \<open>
   A (multiplicative) character is a completely multiplicative function from a group to the
   complex numbers. For simplicity, we restrict this to finite abelian groups here, which is
   the most interesting case.
 
   Characters form a group where the identity is the \emph{principal} character that maps all
   elements to $1$, multiplication is point-wise multiplication of the characters, and the inverse
   is the point-wise complex conjugate.
 
   This group is often called the \emph{Pontryagin dual} group and is isomorphic to the original
   group (in a non-natural way) while the double-dual group \<^emph>\<open>is\<close> naturally isomorphic to the
   original group.
 
   To get extensionality of the characters, we also require characters to map anything that is
   not in the group to $0$.
 \<close>
 
 definition principal_char :: "('a, 'b) monoid_scheme \<Rightarrow> 'a \<Rightarrow> complex" where
   "principal_char G a = (if a \<in> carrier G then 1 else 0)"
 
 definition inv_character where
   "inv_character \<chi> = (\<lambda>a. cnj (\<chi> a))"
 
 lemma inv_character_principal [simp]: "inv_character (principal_char G) = principal_char G"
   by (simp add: inv_character_def principal_char_def fun_eq_iff)
 
 lemma inv_character_inv_character [simp]: "inv_character (inv_character \<chi>) = \<chi>"
   by (simp add: inv_character_def)
 
 lemma eval_inv_character: "inv_character \<chi> j = cnj (\<chi> j)"
   by (simp add: inv_character_def)
 
 
 bundle character_syntax
 begin
 notation principal_char ("\<chi>\<^sub>0\<index>")
 end
 
 locale character = finite_comm_group +
   fixes \<chi> :: "'a \<Rightarrow> complex"
   assumes char_one_nz: "\<chi> \<one> \<noteq> 0"
   assumes char_eq_0:   "a \<notin> carrier G \<Longrightarrow> \<chi> a = 0"
   assumes char_mult [simp]: "a \<in> carrier G \<Longrightarrow> b \<in> carrier G \<Longrightarrow> \<chi> (a \<otimes> b) = \<chi> a * \<chi> b"
 begin
 
 
 subsection \<open>Basic properties\<close>
 
 lemma char_one [simp]: "\<chi> \<one> = 1"
 proof-
   from char_mult[of \<one> \<one>] have "\<chi> \<one> * (\<chi> \<one> - 1) = 0"
     by (auto simp del: char_mult)
   with char_one_nz show ?thesis by simp
 qed
 
 lemma char_power [simp]: "a \<in> carrier G \<Longrightarrow> \<chi> (a [^] k) = \<chi> a ^ k"
   by (induction k) auto
 
 lemma char_root:
   assumes "a \<in> carrier G"
   shows   "\<chi> a ^ ord a = 1"
 proof -
   from assms have "\<chi> a ^ ord a = \<chi> (a [^] ord a)"
     by (subst char_power) auto
   also from fin and assms have "a [^] ord a = \<one>" by (intro pow_ord_eq_1) auto
   finally show ?thesis by simp
 qed
 
 lemma char_root':
   assumes "a \<in> carrier G"
   shows   "\<chi> a ^ order G = 1"
 proof -
   from assms have "\<chi> a ^ order G = \<chi> (a [^] order G)" by simp
   also from fin and assms have "a [^] order G = \<one>" by (intro pow_order_eq_1) auto
   finally show ?thesis by simp
 qed
 
 lemma norm_char: "norm (\<chi> a) = (if a \<in> carrier G then 1 else 0)"
 proof (cases "a \<in> carrier G")
   case True
   have "norm (\<chi> a) ^ order G = norm (\<chi> a ^ order G)" by (simp add: norm_power)
   also from True have "\<chi> a ^ order G = 1" by (rule char_root')
   finally have "norm (\<chi> a) ^ order G = 1 ^ order G" by simp
   hence "norm (\<chi> a) = 1" by (subst (asm) power_eq_iff_eq_base) auto
   with True show ?thesis by auto
 next
   case False
   thus ?thesis by (auto simp: char_eq_0)
 qed
 
 lemma char_eq_0_iff: "\<chi> a = 0 \<longleftrightarrow> a \<notin> carrier G"
 proof -
   have "\<chi> a = 0 \<longleftrightarrow> norm (\<chi> a) = 0" by simp
   also have "\<dots> \<longleftrightarrow> a \<notin> carrier G" by (subst norm_char) auto
   finally show ?thesis .
 qed
 
 lemma inv_character: "character G (inv_character \<chi>)"
   by standard (auto simp: inv_character_def char_eq_0)
 
 lemma mult_inv_character: "\<chi> k * inv_character \<chi> k = principal_char G k"
 proof -
   have "\<chi> k * inv_character \<chi> k = of_real (norm (\<chi> k) ^ 2)"
     by (subst complex_norm_square) (simp add: inv_character_def)
   also have "\<dots> = principal_char G k"
     by (simp add: principal_char_def norm_char)
   finally show ?thesis .
 qed
 
 lemma
   assumes "a \<in> carrier G"
   shows    char_inv: "\<chi> (inv a) = cnj (\<chi> a)" and char_inv': "\<chi> (inv a) = inverse (\<chi> a)"
 proof -
   from assms have "inv a \<otimes> a = \<one>" by simp
   also have "\<chi> \<dots> = 1" by simp
   also from assms have "\<chi> (inv a \<otimes> a) = \<chi> (inv a) * \<chi> a"
     by (intro char_mult) auto
   finally have *: "\<chi> (inv a) * \<chi> a = 1" .
   thus "\<chi> (inv a) = inverse (\<chi> a)" by (auto simp: divide_simps)
   also from mult_inv_character[of a] and assms have "inverse (\<chi> a) = cnj (\<chi> a)"
     by (auto simp add: inv_character_def principal_char_def divide_simps mult.commute)
   finally show "\<chi> (inv a) = cnj (\<chi> a)" .
 qed
 
 end
 
 lemma (in finite_comm_group) character_principal [simp, intro]: "character G (principal_char G)"
   by standard (auto simp: principal_char_def)
 
 lemmas [simp,intro] = finite_comm_group.character_principal
 
 lemma character_ext:
   assumes "character G \<chi>" "character G \<chi>'" "\<And>x. x \<in> carrier G \<Longrightarrow> \<chi> x = \<chi>' x"
   shows   "\<chi> = \<chi>'"
 proof
   fix x :: 'a
   show "\<chi> x = \<chi>' x"
     using assms by (cases "x \<in> carrier G") (auto simp: character.char_eq_0)
 qed
 
 lemma character_mult [intro]: 
   assumes "character G \<chi>" "character G \<chi>'"
   shows   "character G (\<lambda>x. \<chi> x * \<chi>' x)"
 proof -
   interpret \<chi>: character G \<chi> by fact
   interpret \<chi>': character G \<chi>' by fact
   show ?thesis by standard (auto simp: \<chi>.char_eq_0)
 qed
  
 
 lemma character_inv_character_iff [simp]: "character G (inv_character \<chi>) \<longleftrightarrow> character G \<chi>"
 proof
   assume "character G (inv_character \<chi>)"
   from character.inv_character [OF this] show "character G \<chi>" by simp
 qed (auto simp: character.inv_character)
 
 
 definition characters :: "('a, 'b) monoid_scheme \<Rightarrow> ('a \<Rightarrow> complex) set"  where
   "characters G = {\<chi>. character G \<chi>}"
 
 
 subsection \<open>The Character group\<close>
 
 text \<open>
   The characters of a finite abelian group $G$ form another group $\widehat{G}$, which is called
   its Pontryagin dual group. This generalises to the more general setting of locally compact
   abelian groups, but we restrict ourselves to the finite setting because it is much easier.
 \<close>
 definition Characters :: "('a, 'b) monoid_scheme \<Rightarrow> ('a \<Rightarrow> complex) monoid"
-  where "Characters G = \<lparr> carrier = characters G, mult = (\<lambda>\<chi>\<^sub>1 \<chi>\<^sub>2 k. \<chi>\<^sub>1 k * \<chi>\<^sub>2 k),
+  where "Characters G = \<lparr> carrier = characters G, monoid.mult = (\<lambda>\<chi>\<^sub>1 \<chi>\<^sub>2 k. \<chi>\<^sub>1 k * \<chi>\<^sub>2 k),
                           one = principal_char G \<rparr>"
 
 lemma carrier_Characters: "carrier (Characters G) = characters G"
   by (simp add: Characters_def)
 
 lemma one_Characters: "one (Characters G) = principal_char G"
   by (simp add: Characters_def)
 
-lemma mult_Characters: "mult (Characters G) \<chi>\<^sub>1 \<chi>\<^sub>2 = (\<lambda>a. \<chi>\<^sub>1 a * \<chi>\<^sub>2 a)"
+lemma mult_Characters: "monoid.mult (Characters G) \<chi>\<^sub>1 \<chi>\<^sub>2 = (\<lambda>a. \<chi>\<^sub>1 a * \<chi>\<^sub>2 a)"
   by (simp add: Characters_def)
 
 context finite_comm_group
 begin
 
 sublocale principal: character G "principal_char G" ..
 
 lemma finite_characters [intro]: "finite (characters G)"
 proof (rule finite_subset)
   show "characters G \<subseteq> (\<lambda>f x. if x \<in> carrier G then f x else 0) ` 
                           Pi\<^sub>E (carrier G) (\<lambda>_. {z. z ^ order G = 1})" (is "_ \<subseteq> ?h ` ?Chars")
   proof (intro subsetI, goal_cases)
     case (1 \<chi>)
     then interpret \<chi>: character G \<chi> by (simp add: characters_def)
     have "?h (restrict \<chi> (carrier G)) \<in> ?h ` ?Chars"
       by (intro imageI) (auto simp: \<chi>.char_root')
     also have "?h (restrict \<chi> (carrier G)) = \<chi>" by (simp add: fun_eq_iff \<chi>.char_eq_0)
     finally show ?case .
   qed
   show "finite (?h ` ?Chars)"
     by (intro finite_imageI finite_PiE finite_roots_unity) (auto simp: Suc_le_eq)
 qed
 
 lemma finite_comm_group_Characters [intro]: "finite_comm_group (Characters G)"
 proof
   fix \<chi> \<chi>' assume *: "\<chi> \<in> carrier (Characters G)" "\<chi>' \<in> carrier (Characters G)"
   from * interpret \<chi>: character G \<chi> by (simp_all add: characters_def carrier_Characters)
   from * interpret \<chi>': character G \<chi>' by (simp_all add: characters_def  carrier_Characters)
   have "character G (\<lambda>k. \<chi> k * \<chi>' k)"
     by standard (insert *, simp_all add: \<chi>.char_eq_0 one_Characters 
                                          mult_Characters characters_def  carrier_Characters)
   thus "\<chi> \<otimes>\<^bsub>Characters G\<^esub> \<chi>' \<in> carrier (Characters G)"
     by (simp add: characters_def one_Characters mult_Characters  carrier_Characters)
 next
   have "character G (principal_char G)" ..
   thus "\<one>\<^bsub>Characters G\<^esub> \<in> carrier (Characters G)"
     by (simp add: characters_def one_Characters mult_Characters  carrier_Characters)
 next
   fix \<chi> assume *: "\<chi> \<in> carrier (Characters G)"
   from * interpret \<chi>: character G \<chi> by (simp_all add: characters_def carrier_Characters)
   show "\<one>\<^bsub>Characters G\<^esub> \<otimes>\<^bsub>Characters G\<^esub> \<chi> = \<chi>" and "\<chi> \<otimes>\<^bsub>Characters G\<^esub> \<one>\<^bsub>Characters G\<^esub> = \<chi>"
     by (simp_all add: principal_char_def fun_eq_iff \<chi>.char_eq_0 one_Characters mult_Characters)
 next
   have "\<chi> \<in> Units (Characters G)" if "\<chi> \<in> carrier (Characters G)" for \<chi>
   proof -
     from that interpret \<chi>: character G \<chi> by (simp add: characters_def carrier_Characters)
     have "\<chi> \<otimes>\<^bsub>Characters G\<^esub> inv_character \<chi> = \<one>\<^bsub>Characters G\<^esub>" and 
          "inv_character \<chi> \<otimes>\<^bsub>Characters G\<^esub> \<chi> = \<one>\<^bsub>Characters G\<^esub>"
       by (simp_all add: \<chi>.mult_inv_character mult_ac one_Characters mult_Characters)
     moreover from that have "inv_character \<chi> \<in> carrier (Characters G)"
       by (simp add: characters_def carrier_Characters)
     ultimately show ?thesis using that unfolding Units_def by blast
   qed
   thus "carrier (Characters G) \<subseteq> Units (Characters G)" ..
 qed (auto simp: principal_char_def one_Characters mult_Characters carrier_Characters)
 
 end
 
 lemma (in character) character_in_order_1:
   assumes "order G = 1"
   shows   "\<chi> = principal_char G"
 proof -
   from assms have "card (carrier G - {\<one>}) = 0"
     by (subst card_Diff_subset) (auto simp: order_def)
   hence "carrier G - {\<one>} = {}"
     by (subst (asm) card_0_eq) auto
   hence "carrier G = {\<one>}" by auto
   thus ?thesis
     by (intro ext) (simp_all add: principal_char_def char_eq_0)
 qed
 
 lemma (in finite_comm_group) characters_in_order_1:
   assumes "order G = 1"
   shows   "characters G = {principal_char G}"
   using character.character_in_order_1 [OF _ assms] by (auto simp: characters_def)
 
 lemma (in character) inv_Characters: "inv\<^bsub>Characters G\<^esub> \<chi> = inv_character \<chi>"
 proof -
   interpret Characters: finite_comm_group "Characters G" ..
   have "character G \<chi>" ..
   thus ?thesis
     by (intro Characters.inv_equality) 
        (auto simp: characters_def mult_inv_character mult_ac 
                    carrier_Characters one_Characters mult_Characters)
 qed
 
 lemma (in finite_comm_group) inv_Characters': 
   "\<chi> \<in> characters G \<Longrightarrow> inv\<^bsub>Characters G\<^esub> \<chi> = inv_character \<chi>"
   by (intro character.inv_Characters) (auto simp: characters_def)
 
 lemmas (in finite_comm_group) Characters_simps = 
   carrier_Characters mult_Characters one_Characters inv_Characters'
 
 lemma inv_Characters': "\<chi> \<in> characters G \<Longrightarrow> inv\<^bsub>Characters G\<^esub> \<chi> = inv_character \<chi>"
   using character.inv_Characters[of G \<chi>] by (simp add: characters_def)
 
-
-
-subsection \<open>Relationship of characters and adjoining\<close>
-
-text \<open>
-  We now study the set of characters of two subgroups $H$ and $H_x$, where $x\in G\setminus H$
-  and $H_x$ is the smallest supergroup of $H$ that contains \<open>x\<close>.
-
-  Let $n$ denote the indicator of \<open>x\<close> in \<open>H\<close> (i.\,e.\ the smallest positive number such
-  that $x^n\in H$) We show that any character on $H_x$ corresponds to a pair of
-  a character \<open>\<chi>\<close> on \<open>H\<close> and an $n$-th root of $\chi(x^n)$ (or, equivalently, an $n$-th
-  root of unity).
-\<close>
-
-context finite_comm_group_adjoin
-begin
+subsection \<open>The isomorphism between a group and its dual\<close>
 
-lemma lower_character:
-  assumes "character (G\<lparr>carrier := adjoin G H a\<rparr>) \<chi>" 
-    (is "character ?G'' _")
-  shows   "character (G\<lparr>carrier := H\<rparr>) (\<lambda>x. if x \<in> H then \<chi> x else 0)" (is "character ?G' ?\<chi>")
+text \<open>We start this section by inspecting the special case of a cyclic group. Here, any character
+is fixed by the value it assigns to the generating element of the cyclic group. This can then be
+used to construct a bijection between the nth unit roots and the elements of the character group -
+implying the other results.\<close>
+
+lemma (in finite_cyclic_group)
+  defines ic: "induce_char \<equiv> (\<lambda>c::complex. (\<lambda>a. if a\<in>carrier G then c powi get_exp gen a else 0))"
+  shows order_Characters: "order (Characters G) = order G"
+  and   gen_fixes_char: "\<lbrakk>character G a; character G b; a gen = b gen\<rbrakk> \<Longrightarrow> a = b"
+  and   unity_root_induce_char: "z ^ order G = 1 \<Longrightarrow> character G (induce_char z)"
 proof -
-  have "subgroup H G" ..
-  then interpret G'': finite_comm_group ?G'' 
-    by (intro subgroup_imp_finite_comm_group adjoin_subgroup) auto
-  from \<open>subgroup H G\<close> interpret G': finite_comm_group ?G'
-    by (intro subgroup_imp_finite_comm_group adjoin_subgroup) auto
-  from assms interpret character ?G'' \<chi>
-    by (simp add: characters_def)
-  show ?thesis
+  interpret C: finite_comm_group "Characters G" using finite_comm_group_Characters . 
+  define n where "n = order G"
+  hence n: "n > 0" using order_gt_0 by presburger
+  from n_def have nog: "n = ord gen" using ord_gen_is_group_order by simp
+  have xnz: "x \<noteq> 0" if "x ^ n = 1" for x::complex using n(1) that by (metis zero_neq_one zero_power)
+  have m: "x powi m = x powi (m mod n)" if "x ^ n = 1" for x::complex and m::int
+    using powi_mod[OF that n] .
+  show cf: "character G (induce_char x)" if x: "x ^ n = 1" for x
   proof
-    fix x y assume "x \<in> carrier ?G'" "y \<in> carrier ?G'"
-    thus "?\<chi> (x \<otimes>\<^bsub>?G'\<^esub> y) = ?\<chi> x * ?\<chi> y"
-      using char_mult[of x y] mem_adjoin[OF \<open>subgroup H G\<close>] by auto
-  qed (insert char_one, auto simp del: char_one)
+    show "induce_char x \<one> \<noteq> 0" using xnz[OF that] unfolding ic by auto
+    show "induce_char x a = 0" if "a \<notin> carrier G" for a using that unfolding ic by simp
+    show "induce_char x (a \<otimes> b) = induce_char x a * induce_char x b"
+      if "a \<in> carrier G" "b \<in> carrier G" for a b
+    proof -
+      have "x powi get_exp gen (a \<otimes> b) = x powi get_exp gen a * x powi get_exp gen b"
+      proof -
+        have "x powi get_exp gen (a \<otimes> b) = x powi ((get_exp gen a + get_exp gen b) mod n)"
+          using m[OF x] get_exp_mult_mod[OF that] n_def ord_gen_is_group_order by metis
+        also have "\<dots> = x powi (get_exp gen a + get_exp gen b)" using m[OF x] by presburger
+        finally show ?thesis by (simp add: power_int_add xnz[OF x])
+      qed
+      thus ?thesis using that unfolding ic by simp
+    qed
+  qed
+  define get_c where gc: "get_c = (\<lambda>c::'a \<Rightarrow> complex. c gen)"
+  have biji: "bij_betw induce_char {z. z ^ n = 1} (characters G)"
+   and bijg: "bij_betw get_c (characters G) {z. z ^ n = 1}"
+  proof (intro bij_betwI[of _ _ _ get_c])
+    show iin: "induce_char \<in> {z. z ^ n = 1} \<rightarrow> characters G" using cf unfolding characters_def
+      by blast
+    show gi: "get_c (induce_char x) = x" if "x \<in> {z. z ^ n = 1}" for x
+    proof (cases "n = 1")
+      case True
+      with that have "x = 1" by force
+      thus ?thesis unfolding ic gc by simp
+    next
+      case False
+      have x: "x ^ n = 1" using that by blast
+      have "x powi get_exp gen gen = x"
+      proof -
+        have "x powi get_exp gen gen = x powi (get_exp gen gen mod n)" using m[OF x] by blast
+        moreover have "(get_exp gen gen mod n) = 1"
+        proof -
+          have "1 = 1 mod int n" using False n by auto
+          also have "\<dots> = get_exp gen gen mod n"
+            by (unfold nog, intro pow_eq_int_mod[OF gen_closed],
+                use get_exp_fulfills[OF gen_closed] in auto)
+          finally show ?thesis by argo
+        qed
+        ultimately show "x powi get_exp gen gen = x" by simp
+      qed
+      thus ?thesis unfolding ic gc by simp
+    qed
+    show gin: "get_c \<in> characters G \<rightarrow> {z. z ^ n = 1}"
+    proof -
+      have "False" if "get_c c ^ n \<noteq> 1" "character G c" for c
+      proof -
+        interpret character G c by fact
+        show False using that(1)[unfolded gc] by (simp add: char_root' n_def)
+      qed
+      thus ?thesis unfolding characters_def by blast
+    qed
+    show ig: "induce_char (get_c y) = y" if y: "y \<in> characters G" for y
+    proof (cases "n = 1")
+      case True
+      hence "y = principal_char G" using y n_def character.character_in_order_1 characters_def
+        by auto
+      thus ?thesis unfolding ic gc principal_char_def by force
+    next
+      case False
+      have yc: "y \<in> carrier (Characters G)" using y[unfolded carrier_Characters[symmetric]] .
+      interpret character G y using that unfolding characters_def by simp
+      have ygo: "y gen ^ n = 1" using char_root'[OF gen_closed] n_def by blast
+      have "y gen powi get_exp gen a = y a" if "a \<in> carrier G" for a using that
+      proof(induction rule: generator_induct1)
+        case gen
+        have "y gen powi get_exp gen gen = y gen powi (get_exp gen gen mod n)"
+          using m[OF ygo] by blast
+        also have "\<dots> = y gen powi ((1::int) mod n)"
+          using get_exp_self[OF gen_closed] nog by argo
+        also have "\<dots> = y gen powi 1" using False n by simp
+        finally have yg: "y gen powi get_exp gen gen = y gen" by simp
+        thus ?case .
+        case (step x)
+        have "y gen powi get_exp gen (x \<otimes> gen) = y gen powi (get_exp gen (x \<otimes> gen) mod n)"
+          using m[OF ygo] by blast
+        also have "\<dots> = y gen powi ((get_exp gen x + get_exp gen gen) mod n)"
+          using get_exp_mult_mod[OF step(1) gen_closed, unfolded nog[symmetric]] by argo
+        also have "\<dots> = y gen powi (get_exp gen x + get_exp gen gen)" using m[OF ygo] by presburger
+        also have "\<dots> = y gen powi get_exp gen x * y gen powi get_exp gen gen"
+          by (simp add: char_eq_0_iff power_int_add)
+        also have "\<dots> = y x * y gen" using yg step(2) by argo
+        also have "\<dots> = y (x \<otimes> gen)" using step(1) by simp
+        finally show ?case .
+      qed
+      thus "induce_char (get_c y) = y" unfolding ic gc using char_eq_0 by auto
+    qed
+    show "bij_betw get_c (characters G) {z. z ^ n = 1}" using ig gi iin gin
+      by (auto intro: bij_betwI)
+  qed
+  with card_roots_unity_eq[OF n] n_def show "order (Characters G) = order G" unfolding order_def
+    by (metis bij_betw_same_card carrier_Characters)
+  assume assm: "character G a" "character G b" "a gen = b gen"
+  with bijg[unfolded gc characters_def bij_betw_def inj_on_def] show "a = b" by auto
 qed
 
-definition lift_character :: "('a \<Rightarrow> complex) \<times> complex \<Rightarrow> ('a \<Rightarrow> complex)" where
-  "lift_character = 
-     (\<lambda>(\<chi>,z) x. if x \<in> adjoin G H a then \<chi> (fst (unadjoin x)) * z ^ snd (unadjoin x) else 0)"
+text \<open>Moreover, we can show that a character that assigns a "true" root of unity to the
+generating element of the group, generates the character group.\<close>
 
-lemma lift_character:
-  defines "h \<equiv> subgroup_indicator G H a"
-  assumes "character (G\<lparr>carrier := H\<rparr>) \<chi>" (is "character ?G' _") and "z ^ h = \<chi> (a [^] h)"
-  shows   "character (G\<lparr>carrier := adjoin G H a\<rparr>) (lift_character (\<chi>, z))" (is "character ?G'' _")
+lemma (in finite_cyclic_group) finite_cyclic_group_Characters:
+  obtains \<chi> where "finite_cyclic_group (Characters G) \<chi>"
 proof -
-  interpret H': subgroup "adjoin G H a" G by (intro adjoin_subgroup is_subgroup) auto
-  have "subgroup H G" ..
-  then interpret G'': finite_comm_group ?G''
-    by (intro subgroup_imp_finite_comm_group adjoin_subgroup) auto
-  from \<open>subgroup H G\<close> interpret G': finite_comm_group ?G'
-    by (intro subgroup_imp_finite_comm_group adjoin_subgroup) auto
-  from assms interpret character ?G' \<chi> by (simp add: characters_def)
-  show ?thesis
-  proof (standard, goal_cases)
-    case 1
-    from char_one show ?case
-      by (auto simp: lift_character_def simp del: char_one)
-  next
-    case (2 x)
-    thus ?case by (auto simp: lift_character_def)
-  next
-    case (3 x y)
-    from 3(1) obtain x' k where x: "x' \<in> H" "x = x' \<otimes> a [^] k" and k: "k < h"
-      by (auto simp: adjoin_def h_def)
-    from 3(2) obtain y' l where y: "y' \<in> H" "y = y' \<otimes> a [^] l" and l: "l < h"
-      by (auto simp: adjoin_def h_def)
-    have [simp]: "unadjoin x = (x', k)" using x k by (intro unadjoin_unique') (auto simp: h_def)
-    have [simp]: "unadjoin y = (y', l)" using y l by (intro unadjoin_unique') (auto simp: h_def)
-    have char_mult': "\<chi> (x \<otimes> y) = \<chi> x * \<chi> y" if "x \<in> H" "y \<in> H" for x y
-      using char_mult[of x y] that by simp
-    have char_power': "\<chi> (x [^] n) = \<chi> x ^ n" if "x \<in> H" for x n
-      using that char_one by (induction n) (simp_all add: char_mult' del: char_one)
-
-    define r where "r = (k + l) mod h"
-    have r: "r < subgroup_indicator G H a" unfolding h_def r_def
-      by (intro mod_less_divisor subgroup_indicator_pos is_subgroup) auto
-    define zz where "zz = (a [^] h) [^] ((k + l) div h)"
-    have [simp]: "zz \<in> H" unfolding zz_def h_def 
-      by (rule nat_pow_closed) (auto intro: pow_subgroup_indicator is_subgroup)
-    have "a [^] k \<otimes> a [^] l = zz \<otimes> a [^] r"
-      by (simp add: nat_pow_mult zz_def nat_pow_pow r_def)
-    with x y r have "unadjoin (x \<otimes> y) = (x' \<otimes> y' \<otimes> zz, r)"
-      by (intro unadjoin_unique' m_closed) (auto simp: m_ac)
-    hence "lift_character (\<chi>, z) (x \<otimes>\<^bsub>?G''\<^esub> y) = \<chi> (x' \<otimes> y' \<otimes> zz) * z ^ r"
-      using 3 by (simp add: lift_character_def)
-    also have "\<dots> = \<chi> x' * \<chi> y' * (\<chi> zz * z ^ r)"
-      using x(1) y(1) by (simp add: char_mult' char_power')
-    also have "\<chi> zz * z ^ r = z ^ (h * ((k + l) div h) + r)"
-      unfolding h_def zz_def using \<open>subgroup H G\<close> assms(3)[symmetric] 
-      by (subst char_power') (auto simp: pow_subgroup_indicator h_def power_mult power_add)
-    also have "h * ((k + l) div h) + r = k + l" by (simp add: r_def)
-    also have "\<chi> x' * \<chi> y' * z ^ (k + l) = lift_character (\<chi>,z) x * lift_character (\<chi>,z) y"
-      using 3 by (simp add: lift_character_def power_add)
-    finally show ?case .
+  interpret C: finite_comm_group "Characters G" by (rule finite_comm_group_Characters)
+  define n where n: "n = order G"
+  hence nnz: "n \<noteq> 0" by blast
+  from n have nog: "n = ord gen" using ord_gen_is_group_order by simp
+  obtain x::complex where x: "x ^ n = 1" "\<And>m. \<lbrakk>0<m; m<n\<rbrakk> \<Longrightarrow> x ^ m \<noteq> 1"
+    using true_nth_unity_root by blast
+  have xnz: "x \<noteq> 0" using x n by (metis order_gt_0 zero_neq_one zero_power)
+  have m: "x powi m = x powi (m mod n)" for m::int
+    using powi_mod[OF x(1)] nnz by blast
+  let ?f = "(\<lambda>a. if a \<in> carrier G then x powi (get_exp gen a) else 0)"
+  have cf: "character G ?f" using unity_root_induce_char[OF x(1)[unfolded n]] .
+  have fpow: "(?f [^]\<^bsub>Characters G\<^esub> m) a = x powi ((get_exp gen a) * m)"
+    if "a \<in> carrier G" for a::'a and m::nat
+    using that
+  proof(unfold Characters_def principal_char_def, induction m)
+    case s: (Suc m)
+    have "x powi (get_exp gen a * int m) * x powi get_exp gen a
+        = x powi (get_exp gen a * (1 + int m))"
+    proof -
+      fix ma :: nat
+      have "x powi ((1 + int ma) * get_exp gen a)
+          = x powi (get_exp gen a + int ma * get_exp gen a) \<and> 0 \<noteq> x"
+        by (simp add: comm_semiring_class.distrib xnz)
+      then show "x powi (get_exp gen a * int ma) * x powi get_exp gen a
+               = x powi (get_exp gen a * (1 + int ma))"
+        by (simp add: mult.commute power_int_add)
+    qed
+    thus ?case using s by simp
+  qed simp
+  interpret cyclic_group "Characters G" ?f
+  proof (intro C.element_ord_generates_cyclic)
+    show fc: "?f \<in> carrier (Characters G)" using cf carrier_Characters[of G] characters_def by fast
+    from x nnz have fno: "?f [^]\<^bsub>Characters G\<^esub> m \<noteq> \<one>\<^bsub>Characters G\<^esub>" if "0 < m" "m < n" for m
+    proof (cases "n = 1")
+      case False
+      have "\<one>\<^bsub>Characters G\<^esub> gen = 1" unfolding Characters_def principal_char_def using that by simp
+      moreover have "(?f [^]\<^bsub>Characters G\<^esub> m) gen \<noteq> 1"
+      proof -
+        have "(?f [^]\<^bsub>Characters G\<^esub> m) gen = x powi ((get_exp gen gen) * m)" using fpow by blast
+        also have "\<dots> = (x powi (get_exp gen gen)) ^ m" by (simp add: power_int_mult)
+        also have "\<dots> = x ^ m"
+        proof -
+          have "x powi (get_exp gen gen) = x powi ((get_exp gen gen) mod n)" using m by blast
+          moreover have "((get_exp gen gen) mod n) = 1"
+          proof -
+            have "1 = 1 mod int n" using False nnz by simp
+            also have "\<dots> = get_exp gen gen mod n"
+              by (unfold nog, intro pow_eq_int_mod[OF gen_closed],
+                  use get_exp_fulfills[OF gen_closed] in auto)
+            finally show ?thesis by argo
+          qed
+          ultimately have "x powi (get_exp gen gen) = x" by simp
+          thus ?thesis by simp
+        qed
+        finally show ?thesis using x(2)[OF that] by argo
+      qed
+      ultimately show ?thesis by fastforce
+    qed (use that in blast)
+    have "C.ord ?f = n"
+    proof -
+      from nnz have "C.ord ?f \<le> n" unfolding n
+        using C.ord_dvd_group_order[OF fc] order_Characters dvd_nat_bounds by auto
+      with C.ord_conv_Least[OF fc] C.pow_order_eq_1[OF fc] n nnz show "C.ord ?f = n"
+        by (metis (no_types, lifting) C.ord_pos C.pow_ord_eq_1 fc fno le_neq_implies_less)
+    qed
+    thus "C.ord ?f = order (Characters G)" using n order_Characters by argo
   qed
+  have "finite_cyclic_group (Characters G) ?f" by unfold_locales
+  with that show ?thesis by blast
 qed
 
-lemma lower_character_lift_character:
-  assumes "\<chi> \<in> characters (G\<lparr>carrier := H\<rparr>)"
-  shows   "(\<lambda>x. if x \<in> H then lift_character (\<chi>, z) x else 0) = \<chi>" (is ?th1)
-          "lift_character (\<chi>, z) a = z" (is ?th2)
+text \<open>And as two cyclic groups of the same order are isomorphic it follows the isomorphism of a
+finite cyclic group and its dual.\<close>
+
+lemma (in finite_cyclic_group) Characters_iso:
+  "G \<cong> Characters G"
 proof -
-  from assms interpret \<chi>: character "G\<lparr>carrier := H\<rparr>" \<chi> by (simp add: characters_def)
-  have char_mult: "\<chi> (x \<otimes> y) = \<chi> x * \<chi> y" if "x \<in> H" "y \<in> H" for x y
-    using \<chi>.char_mult[of x y] that by simp
-  have char_power: "\<chi> (x [^] n) = \<chi> x ^ n" if "x \<in> H" for x n
-    using \<chi>.char_one that by (induction n) (simp_all add: char_mult)
-  show ?th1 using \<chi>.char_eq_0 mem_adjoin[OF is_subgroup _ a_in_carrier]
-    by (auto simp: lift_character_def)
-  show ?th2 using \<chi>.char_one is_subgroup
-    by (auto simp: lift_character_def adjoined_in_adjoin)
+  from finite_cyclic_group_Characters obtain f where f: "finite_cyclic_group (Characters G) f" .
+  then interpret C: finite_cyclic_group "Characters G" f .
+  have "cyclic_group (Characters G) f" by unfold_locales
+  from iso_cyclic_groups_same_order[OF this order_Characters[symmetric]] show ?thesis .
 qed
 
-lemma lift_character_lower_character:
-  assumes "\<chi> \<in> characters (G\<lparr>carrier := adjoin G H a\<rparr>)"
-  shows   "lift_character (\<lambda>x. if x \<in> H then \<chi> x else 0, \<chi> a) = \<chi>"
+text \<open>The character groups of two isomorphic groups are also isomorphic.\<close>
+
+lemma (in finite_comm_group) iso_imp_iso_chars:
+  assumes "G \<cong> H" "group H"
+  shows "Characters G \<cong> Characters H"
 proof -
-  let ?G' = "G\<lparr>carrier := adjoin G H a\<rparr>"
-  from assms interpret \<chi>: character ?G' \<chi> by (simp add: characters_def)
+  interpret H: finite_comm_group H by (rule iso_imp_finite_comm[OF assms])
+  from assms have "H \<cong> G" using iso_sym by auto
+  then obtain g where g: "g \<in> iso H G" unfolding is_iso_def by blast
+  then interpret ggh: group_hom H G g by (unfold_locales, unfold iso_def, simp)
+  let ?f = "(\<lambda>c a. if a \<in> carrier H then (c \<circ> g) a else 0)"
+  have "?f \<in> iso (Characters G) (Characters H)"
+  proof (intro isoI)
+    interpret CG: finite_comm_group "Characters G" by (intro finite_comm_group_Characters)
+    interpret CH: finite_comm_group "Characters H" by (intro H.finite_comm_group_Characters)
+    have f_in: "?f x \<in> carrier (Characters H)" if "x \<in> carrier (Characters G)" for x
+    proof (unfold carrier_Characters characters_def, rule, unfold_locales)
+      interpret character G x using that characters_def carrier_Characters by blast
+      show "(if \<one>\<^bsub>H\<^esub> \<in> carrier H then (x \<circ> g) \<one>\<^bsub>H\<^esub> else 0) \<noteq> 0" using g iso_iff by auto
+      show "\<And>a. a \<notin> carrier H \<Longrightarrow> (if a \<in> carrier H then (x \<circ> g) a else 0) = 0" by simp
+      show "?f x (a \<otimes>\<^bsub>H\<^esub> b) = ?f x a * ?f x b" if "a \<in> carrier H" "b \<in> carrier H" for a b
+        using that by auto
+    qed
+    show "?f \<in> hom (Characters G) (Characters H)"
+    proof (intro homI)
+      show "?f x \<in> carrier (Characters H)" if "x \<in> carrier (Characters G)" for x
+        using f_in[OF that] .
+      show "?f (x \<otimes>\<^bsub>Characters G\<^esub> y) = ?f x \<otimes>\<^bsub>Characters H\<^esub> ?f y"
+        if "x \<in> carrier (Characters G)" "y \<in> carrier (Characters G)" for x y
+      proof -
+        interpret x: character G x using that characters_def carrier_Characters by blast
+        interpret y: character G y using that characters_def carrier_Characters by blast
+        show ?thesis using that mult_Characters[of G] mult_Characters[of H] by auto
+      qed
+    qed
+    show "bij_betw ?f (carrier (Characters G)) (carrier (Characters H))"
+    proof(intro bij_betwI)
+      define f where "f = inv_into (carrier H) g"
+      hence f: "f \<in> iso G H" using H.iso_set_sym[OF g] by simp
+      then interpret fgh: group_hom G H f by (unfold_locales, unfold iso_def, simp)
+      let ?g = "(\<lambda>c a. if a \<in> carrier G then (c \<circ> f) a else 0)"
+      show "?f \<in> carrier (Characters G) \<rightarrow> carrier (Characters H)" using f_in by fast
+      show "?g \<in> carrier (Characters H) \<rightarrow> carrier (Characters G)"
+      proof -
+        have g_in: "?g x \<in> carrier (Characters G)" if "x \<in> carrier (Characters H)" for x
+        proof (unfold carrier_Characters characters_def, rule, unfold_locales)
+          interpret character H x using that characters_def carrier_Characters by blast
+          show "(if \<one>\<^bsub>G\<^esub> \<in> carrier G then (x \<circ> f) \<one>\<^bsub>G\<^esub> else 0) \<noteq> 0" using f iso_iff by auto
+          show "\<And>a. a \<notin> carrier G \<Longrightarrow> (if a \<in> carrier G then (x \<circ> f) a else 0) = 0" by simp
+          show "?g x (a \<otimes>\<^bsub>G\<^esub> b) = ?g x a * ?g x b" if "a \<in> carrier G" "b \<in> carrier G" for a b
+            using that by auto
+        qed
+        thus ?thesis by simp
+      qed
+      show "?f (?g x) = x" if x: "x \<in> carrier (Characters H)" for x
+      proof -
+        interpret character H x using x characters_def carrier_Characters by blast
+        have "?f (?g x) a = x a" if a: "a \<notin> carrier H" for a using a char_eq_0[OF a] by auto
+        moreover have "?f (?g x) a = x a" if a: "a \<in> carrier H" for a
+        proof -
+          from a have "inv_into (carrier H) g (g a) = a"
+            by (simp add: g ggh.inj_iff_trivial_ker ggh.iso_kernel)
+          thus ?thesis using a f_def by auto
+        qed
+        ultimately show ?thesis by fast
+      qed
+      show "?g (?f x) = x" if x: "x \<in> carrier (Characters G)" for x
+      proof -
+        interpret character G x using x characters_def carrier_Characters by blast
+        have "?g (?f x) a = x a" if a: "a \<notin> carrier G" for a using a char_eq_0[OF a] by auto
+        moreover have "?g (?f x) a = x a" if a: "a \<in> carrier G" for a using a f_def
+        proof -
+          from a have "g (inv_into (carrier H) g a) = a"
+            by (meson f_inv_into_f g ggh.iso_iff subset_iff)
+          thus ?thesis using a f_def fgh.hom_closed by auto
+        qed
+        ultimately show ?thesis by fast
+      qed
+    qed
+  qed
+  thus ?thesis unfolding is_iso_def by blast
+qed
+
+text \<open>The following two lemmas characterize the way a character behaves in a direct group product:
+a character on the product induces characters on each of the factors. Also, any character on the
+direct product can be decomposed into a pointwise product of characters on the factors.\<close>
+
+lemma DirProds_subchar:
+  assumes "finite_comm_group (DirProds Gs I)"
+  and x: "x \<in> carrier (Characters (DirProds Gs I))" 
+  and i: "i \<in> I"
+  and I: "finite I"
+  defines g: "g \<equiv> (\<lambda>c. (\<lambda>i\<in>I. (\<lambda>a. c ((\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i:=a)))))"
+  shows "character (Gs i) (g x i)"
+proof -
+  interpret DP: finite_comm_group "DirProds Gs I" by fact
+  interpret xc: character "DirProds Gs I" x using x unfolding Characters_def characters_def by auto
+  interpret Gi: finite_comm_group "Gs i"
+    using i DirProds_finite_comm_group_iff[OF I] DP.finite_comm_group_axioms by blast
+  have allg: "\<And>i. i\<in>I \<Longrightarrow> group (Gs i)" using DirProds_group_imp_groups[OF DP.is_group] .
   show ?thesis
-  proof (rule ext, goal_cases)
-    case (1 x)
-    show ?case
-    proof (cases "x \<in> adjoin G H a")
-      case True
-      note * = unadjoin_correct[OF this]
-      interpret H': subgroup "adjoin G H a" G
-        by (intro adjoin_subgroup is_subgroup a_in_carrier)
-      have "x = fst (unadjoin x) \<otimes>\<^bsub>?G'\<^esub> a [^]\<^bsub>?G'\<^esub> snd (unadjoin x)" 
-        using *(3) by (simp add: nat_pow_def)
-      also have "\<chi> \<dots> = \<chi> (fst (unadjoin x)) * \<chi> (a [^]\<^bsub>?G'\<^esub> snd (unadjoin x))"
-        using * is_subgroup by (intro \<chi>.char_mult) 
-                               (auto simp: nat_pow_modify_carrier mem_adjoin adjoined_in_adjoin)
-      also have "\<chi> (a [^]\<^bsub>?G'\<^esub> snd (unadjoin x)) = \<chi> a ^ snd (unadjoin x)"
-        using is_subgroup by (intro \<chi>.char_power) (auto simp: adjoined_in_adjoin)
-      finally show ?thesis using True * by (auto simp: lift_character_def)
-    qed (auto simp: lift_character_def \<chi>.char_eq_0)
+  proof(unfold_locales)
+    have "(\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>) = (\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := \<one>\<^bsub>Gs i\<^esub>)" using i by force
+    thus "g x i \<one>\<^bsub>Gs i\<^esub> \<noteq> 0" using i g DirProds_one''[of Gs I] xc.char_one_nz by auto
+    show "g x i a = 0" if a: "a \<notin> carrier (Gs i)" for a
+    proof -
+      from a i have "((\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := a)) \<notin> carrier (DirProds Gs I)"
+        unfolding DirProds_def by force
+      from xc.char_eq_0[OF this] show ?thesis using i g by auto
+    qed
+    show "g x i (a \<otimes>\<^bsub>Gs i\<^esub> b) = g x i a * g x i b"
+      if ab: "a \<in> carrier (Gs i)" "b \<in> carrier (Gs i)" for a b
+    proof -
+      have "g x i (a \<otimes>\<^bsub>Gs i\<^esub> b)
+          = x ((\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := a) \<otimes>\<^bsub>DirProds Gs I\<^esub> (\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := b))"
+      proof -
+        have "((\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := a) \<otimes>\<^bsub>DirProds Gs I\<^esub> (\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := b))
+            = ((\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := (a \<otimes>\<^bsub>Gs i\<^esub> b)))"
+        proof -
+          have "((\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := a) \<otimes>\<^bsub>DirProds Gs I\<^esub> (\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := b)) j
+              = ((\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := (a \<otimes>\<^bsub>Gs i\<^esub> b))) j"
+            for j
+          proof (cases "j \<in> I")
+            case True
+            from allg[OF True] interpret Gj: group "Gs j" .
+            show ?thesis using ab True i unfolding DirProds_mult by simp
+          next
+            case False
+            then show ?thesis unfolding DirProds_mult using i by fastforce
+          qed
+          thus ?thesis by fast
+        qed
+        thus ?thesis using i g by auto
+      qed 
+      also have "\<dots> = x ((\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := a)) * x ((\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := b))"
+      proof -
+        have ac: "((\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := a)) \<in> carrier (DirProds Gs I)"
+          unfolding DirProds_def using ab i monoid.one_closed[OF group.is_monoid[OF allg]] by force
+        have bc: "((\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := b)) \<in> carrier (DirProds Gs I)"
+          unfolding DirProds_def using ab i monoid.one_closed[OF group.is_monoid[OF allg]] by force
+        from xc.char_mult[OF ac bc] show ?thesis .
+      qed
+      also have "\<dots> = g x i a * g x i b" using i g by auto
+      finally show ?thesis .
+    qed
   qed
 qed
 
-lemma lift_character_unchanged [simp]:
-  assumes "x \<in> H"
-  shows   "lift_character \<chi>z x = fst \<chi>z x"
-  using assms mem_adjoin[of H x a] is_subgroup
-  by (cases \<chi>z) (auto simp: lift_character_def)
-
-lemma lift_character_adjoined [simp]:
- "character (G\<lparr>carrier := H\<rparr>) (fst \<chi>z) \<Longrightarrow> lift_character \<chi>z a = snd \<chi>z"
-  using is_subgroup character.char_one[of "G\<lparr>carrier := H\<rparr>"]
-  by (cases \<chi>z) (auto simp: lift_character_def adjoined_in_adjoin character.char_one)
-
-lemma bij_betw_characters_adjoin:
-  defines "h \<equiv> subgroup_indicator G H a"
-  shows "bij_betw lift_character
-                  (SIGMA \<chi>:characters (G\<lparr>carrier := H\<rparr>). {z. z ^ h = \<chi> (a [^] h)})
-                  (characters (G\<lparr>carrier := adjoin G H a\<rparr>))"
-proof (rule bij_betwI[where ?g = "\<lambda>\<chi>. (\<lambda>x. if x \<in> H then \<chi> x else 0, \<chi> a)"], goal_cases)
-  case 1
-  show ?case by (auto simp: characters_def h_def intro!: lift_character)
-next
-  case 2
-  show ?case unfolding characters_def
-  proof (safe, goal_cases)
-    case (1 \<chi>)
-    thus ?case unfolding h_def by (rule lower_character)
+lemma Characters_DirProds_single_prod:
+  assumes "finite_comm_group (DirProds Gs I)"
+  and x: "x \<in> carrier (Characters (DirProds Gs I))"
+  and I: "finite I"
+  defines g: "g \<equiv> (\<lambda>I. (\<lambda>c. (\<lambda>i\<in>I. (\<lambda>a. c ((\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i:=a))))))"
+  shows "(\<lambda>e. if e\<in>carrier(DirProds Gs I) then \<Prod>i\<in>I. (g I x i) (e i) else 0) = x" (is "?g x = x")
+proof
+  show "?g x e = x e" for e
+  proof (cases "e \<in> carrier (DirProds Gs I)")
+    case True
+    show ?thesis using I x assms(1) True unfolding g
+    proof(induction I arbitrary: x e rule: finite_induct)
+      case empty
+      interpret DP: finite_comm_group "DirProds Gs {}" by fact
+      from DirProds_empty[of Gs] have "order (DirProds Gs {}) = 1" unfolding order_def by simp
+      with DP.characters_in_order_1[OF this] empty(1) show ?case
+        using DirProds_empty[of Gs] unfolding Characters_def principal_char_def by auto
+    next
+      case j: (insert j I)
+      interpret DP: finite_comm_group "DirProds Gs (insert j I)" by fact
+      interpret DP2: finite_comm_group "DirProds Gs I"
+      proof -
+        from DirProds_finite_comm_group_iff[of "insert j I" Gs] DP.finite_comm_group_axioms j
+        have "(\<forall>i\<in>(insert j I). finite_comm_group (Gs i))" by blast
+        with DirProds_finite_comm_group_iff[OF j(1), of Gs] show "finite_comm_group (DirProds Gs I)"
+          by blast
+      qed
+      interpret xc: character "DirProds Gs (insert j I)" x
+        using j(4) unfolding Characters_def characters_def by simp
+      have allg: "\<And>i. i\<in>(insert j I) \<Longrightarrow> group (Gs i)"
+        using DirProds_group_imp_groups[OF DP.is_group] .
+      have e1c: "e(j:= \<one>\<^bsub>Gs j\<^esub>) \<in> carrier (DirProds Gs (insert j I))"
+        using j(6) monoid.one_closed[OF group.is_monoid[OF allg[of j]]]
+        unfolding DirProds_def PiE_def Pi_def by simp
+      have e2c: "(\<lambda>i\<in>(insert j I). \<one>\<^bsub>Gs i\<^esub>)(j := e j) \<in> carrier (DirProds Gs (insert j I))"
+        unfolding DirProds_def PiE_def Pi_def
+        using monoid.one_closed[OF group.is_monoid[OF allg]] comp_in_carr[OF j(6)] by auto
+      have "e = e(j:= \<one>\<^bsub>Gs j\<^esub>) \<otimes>\<^bsub>DirProds Gs (insert j I)\<^esub> (\<lambda>i\<in>(insert j I). \<one>\<^bsub>Gs i\<^esub>)(j := e j)"
+      proof -
+        have "e k
+            = (e(j:= \<one>\<^bsub>Gs j\<^esub>) \<otimes>\<^bsub>DirProds Gs (insert j I)\<^esub> (\<lambda>i\<in>(insert j I). \<one>\<^bsub>Gs i\<^esub>)(j := e j)) k"
+          for k
+        proof(cases "k\<in>(insert j I)")
+          case k: True
+          from allg[OF k] interpret Gk: group "Gs k" .
+          from allg[of j] interpret Gj: group "Gs j" by simp
+          from k show ?thesis unfolding comp_mult[OF k] using comp_in_carr[OF j(6) k] by auto
+        next
+          case False
+          then show ?thesis using j(6) unfolding DirProds_def by auto
+        qed
+        thus ?thesis by blast
+      qed
+      hence "x e = x (e(j:= \<one>\<^bsub>Gs j\<^esub>)) * x ((\<lambda>i\<in>(insert j I). \<one>\<^bsub>Gs i\<^esub>)(j := e j))"
+        using xc.char_mult[OF e1c e2c] by argo
+      also have "\<dots> = (\<Prod>i\<in>I. g (insert j I) x i (e i)) * g (insert j I) x j (e j)"
+      proof -
+        have "x (e(j:= \<one>\<^bsub>Gs j\<^esub>)) = (\<Prod>i\<in>I. g (insert j I) x i (e i))"
+        proof -
+          have eu: "e(j:=undefined) \<in> carrier (DirProds Gs I)" using j(2, 6)
+            unfolding DirProds_def PiE_def Pi_def extensional_def by fastforce
+          let ?x = "\<lambda>p. if p\<in>carrier(DirProds Gs I) then x (p(j:= \<one>\<^bsub>Gs j\<^esub>)) else 0"
+          have cx2: "character (DirProds Gs I) ?x"
+          proof
+            show "?x \<one>\<^bsub>DirProds Gs I\<^esub> \<noteq> 0"
+            proof -
+              have "\<one>\<^bsub>DirProds Gs I\<^esub>(j := \<one>\<^bsub>Gs j\<^esub>) = \<one>\<^bsub>DirProds Gs (insert j I)\<^esub>"
+                unfolding DirProds_one'' by force
+              thus ?thesis by simp
+            qed
+            show "?x a = 0" if a: "a \<notin> carrier (DirProds Gs I)" for a using a by argo
+            show "?x (a \<otimes>\<^bsub>DirProds Gs I\<^esub> b) = ?x a * ?x b"
+              if ab: "a \<in> carrier (DirProds Gs I)" "b \<in> carrier (DirProds Gs I)" for a b
+            proof -
+              have ac: "a(j := \<one>\<^bsub>Gs j\<^esub>) \<in> carrier (DirProds Gs (insert j I))"
+                using ab monoid.one_closed[OF group.is_monoid[OF allg[of j]]]
+                unfolding DirProds_def PiE_def Pi_def by simp
+              have bc: "b(j := \<one>\<^bsub>Gs j\<^esub>) \<in> carrier (DirProds Gs (insert j I))"
+                using ab monoid.one_closed[OF group.is_monoid[OF allg[of j]]]
+                unfolding DirProds_def PiE_def Pi_def by simp
+              have m: "((a \<otimes>\<^bsub>DirProds Gs I\<^esub> b)(j := \<one>\<^bsub>Gs j\<^esub>))
+                     = (a(j := \<one>\<^bsub>Gs j\<^esub>) \<otimes>\<^bsub>DirProds Gs (insert j I)\<^esub> b(j := \<one>\<^bsub>Gs j\<^esub>))"
+              proof -
+                have "((a \<otimes>\<^bsub>DirProds Gs I\<^esub> b)(j := \<one>\<^bsub>Gs j\<^esub>)) h
+                    = (a(j := \<one>\<^bsub>Gs j\<^esub>) \<otimes>\<^bsub>DirProds Gs (insert j I)\<^esub> b(j := \<one>\<^bsub>Gs j\<^esub>)) h"
+                  if h: "h\<in>(insert j I)" for h
+                proof(cases "h=j")
+                  case True
+                  interpret Gj: group "Gs j" using allg[of j] by blast
+                  from True comp_mult[OF h, of Gs "a(j := \<one>\<^bsub>Gs j\<^esub>)" "b(j := \<one>\<^bsub>Gs j\<^esub>)"] show ?thesis
+                    by auto
+                next
+                  case False
+                  interpret Gj: group "Gs h" using allg[OF h] .
+                  from False h comp_mult[OF h, of Gs "a(j := \<one>\<^bsub>Gs j\<^esub>)" "b(j := \<one>\<^bsub>Gs j\<^esub>)"]
+                       comp_mult[of h I Gs a b]
+                  show ?thesis by auto
+                qed
+                moreover have "((a \<otimes>\<^bsub>DirProds Gs I\<^esub> b)(j := \<one>\<^bsub>Gs j\<^esub>)) h
+                             = (a(j := \<one>\<^bsub>Gs j\<^esub>) \<otimes>\<^bsub>DirProds Gs (insert j I)\<^esub> b(j := \<one>\<^bsub>Gs j\<^esub>)) h"
+                  if h: "h\<notin>(insert j I)" for h using h unfolding DirProds_def PiE_def by simp
+                ultimately show ?thesis by blast
+              qed
+              have "x ((a \<otimes>\<^bsub>DirProds Gs I\<^esub> b)(j := \<one>\<^bsub>Gs j\<^esub>))
+                  = x (a(j := \<one>\<^bsub>Gs j\<^esub>)) * x (b(j := \<one>\<^bsub>Gs j\<^esub>))"
+                by (unfold m, intro xc.char_mult[OF ac bc])
+              thus ?thesis using ab by auto
+            qed
+          qed
+          then interpret cx2: character "DirProds Gs I" ?x .
+          from cx2 have cx3:"?x \<in> carrier (Characters (DirProds Gs I))"
+            unfolding Characters_def characters_def by simp
+          from j(3)[OF cx3 DP2.finite_comm_group_axioms eu] have
+           "(if e(j:=undefined) \<in> carrier (DirProds Gs I)
+             then \<Prod>i\<in>I. g I ?x i ((e(j:=undefined)) i)
+             else 0) = ?x (e(j:=undefined))"
+            using eu j(2) unfolding g by fast
+          with eu have "(\<Prod>i\<in>I. g I (\<lambda>p. if p \<in> carrier (DirProds Gs I)
+                                         then x (p(j := \<one>\<^bsub>Gs j\<^esub>))
+                                         else 0) i ((e(j := undefined)) i)) = x (e(j := \<one>\<^bsub>Gs j\<^esub>))"
+            by simp
+          moreover have "g I (\<lambda>a. if a \<in> carrier (DirProds Gs I)
+                                  then x (a(j := \<one>\<^bsub>Gs j\<^esub>))
+                                  else 0) i ((e(j := undefined)) i) = g (insert j I) x i (e i)"
+            if i: "i\<in>I" for i
+          proof -
+            have "(\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := e i) \<in> carrier (DirProds Gs I)"
+              unfolding DirProds_def PiE_def Pi_def extensional_def
+              using monoid.one_closed[OF group.is_monoid[OF allg]] comp_in_carr[OF j(6)] i by simp
+            moreover have "((\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := e i, j := \<one>\<^bsub>Gs j\<^esub>))
+                         = ((\<lambda>i\<in>insert j I. \<one>\<^bsub>Gs i\<^esub>)(i := e i))" using i j(2) by auto
+            ultimately show ?thesis using i j(2, 4, 6) unfolding g by auto
+          qed
+          ultimately show ?thesis by simp
+        qed
+        moreover have "x ((\<lambda>i\<in>(insert j I). \<one>\<^bsub>Gs i\<^esub>)(j := e j)) = g (insert j I) x j (e j)"
+          unfolding g by simp
+        ultimately show ?thesis by argo
+      qed  
+      finally show ?case using j unfolding g by auto
+    qed 
   next
-    case (2 \<chi>)
-    interpret \<chi>: character "G\<lparr>carrier := adjoin G H a\<rparr>" \<chi> by fact
-    have [simp]: "\<chi> (a [^] n) = \<chi> a ^ n" for n using \<chi>.char_power[of a n] is_subgroup 
-      by (auto simp: adjoined_in_adjoin nat_pow_def simp del: \<chi>.char_power)
-    from is_subgroup a_in_carrier pow_subgroup_indicator show ?case
-      by (auto simp: h_def intro!: subgroup_indicator_pos \<chi>.char_eq_0)
+    case False
+    interpret xc: character "DirProds Gs I" x
+      using x unfolding Characters_def characters_def by simp
+    from xc.char_eq_0[OF False] False show ?thesis by argo
   qed
-next
-  case (3 w)
-  thus ?case using lower_character_lift_character[of "fst w" "snd w"]
-    by (auto cong: if_cong)
-next
-  case (4 \<chi>)
-  thus ?case by (rule lift_character_lower_character)
 qed
 
-end
+text \<open>This allows for the following: the character group of a direct product is isomorphic to the
+direct product of the character groups of the factors.\<close>
 
+lemma (in finite_comm_group) Characters_DirProds_iso:
+  assumes "DirProds Gs I \<cong> G" "group (DirProds Gs I)" "finite I"
+  shows "DirProds (Characters \<circ> Gs) I \<cong> Characters G"
+proof -
+  interpret DP: group "DirProds Gs I" by fact
+  interpret DP: finite_comm_group "DirProds Gs I"
+    by (intro iso_imp_finite_comm[OF DP.iso_sym[OF assms(1)]], unfold_locales)
+  interpret DPC: finite_comm_group "DirProds (Characters \<circ> Gs) I"
+    using DirProds_finite_comm_group_iff[OF assms(3), of "Characters \<circ> Gs"]
+          DirProds_finite_comm_group_iff[OF assms(3), of Gs]
+          DP.finite_comm_group_axioms finite_comm_group.finite_comm_group_Characters by auto
+  interpret CDP: finite_comm_group "Characters (DirProds Gs I)"
+    using DP.finite_comm_group_Characters .
+  interpret C: finite_comm_group "Characters G" using finite_comm_group_Characters .
+  have allg: "\<And>i. i\<in>I \<Longrightarrow> group (Gs i)" using DirProds_group_imp_groups[OF assms(2)] .
+  let ?f = "(\<lambda>cp. (\<lambda>e. (if e\<in>carrier (DirProds Gs I) then \<Prod>i\<in>I. cp i (e i) else 0)))"
+  have f_in: "?f x \<in> carrier (Characters (DirProds Gs I))"
+    if x: "x \<in> carrier (DirProds (Characters \<circ> Gs) I)" for x
+  proof(unfold carrier_Characters characters_def, safe, unfold_locales)
+    show "?f x \<one>\<^bsub>DirProds Gs I\<^esub> \<noteq> 0"
+    proof -
+      have "x i (\<one>\<^bsub>DirProds Gs I\<^esub> i) \<noteq> 0" if i: "i \<in> I" for i
+      proof -
+        interpret Gi: finite_comm_group "Gs i"
+          using DirProds_finite_comm_group_iff[OF assms(3)] DP.finite_comm_group_axioms i by blast
+        interpret xi: character "Gs i" "x i"
+          using i x unfolding DirProds_def Characters_def characters_def by auto
+        show ?thesis using DirProds_one'[OF i, of Gs] by simp
+      qed
+      thus ?thesis by (simp add: assms(3))
+    qed
+    show "?f x a = 0" if "a \<notin> carrier (DirProds Gs I)" for a using that by simp
+    show "?f x (a \<otimes>\<^bsub>DirProds Gs I\<^esub> b) = ?f x a * ?f x b"
+      if ab: "a \<in> carrier (DirProds Gs I)" "b \<in> carrier (DirProds Gs I)" for a b
+    proof -
+      have "a \<otimes>\<^bsub>DirProds Gs I\<^esub> b \<in> carrier (DirProds Gs I)" using that by blast
+      moreover have "(\<Prod>i\<in>I. x i ((a \<otimes>\<^bsub>DirProds Gs I\<^esub> b) i))
+                   = (\<Prod>i\<in>I. x i (a i)) * (\<Prod>i\<in>I. x i (b i))"
+      proof -
+        have "x i ((a \<otimes>\<^bsub>DirProds Gs I\<^esub> b) i) = x i (a i) * x i (b i)" if i: "i\<in>I" for i
+        proof -
+          interpret xi: character "Gs i" "x i"
+            using i x unfolding DirProds_def Characters_def characters_def by auto
+          show ?thesis using ab comp_mult[OF i, of Gs a b] by(auto simp: comp_in_carr[OF _ i])
+        qed
+        thus ?thesis using prod.distrib by force
+      qed
+      ultimately show ?thesis using that by auto
+    qed
+  qed
+  have "?f \<in> iso (DirProds (Characters \<circ> Gs) I) (Characters (DirProds Gs I))"
+  proof (intro isoI)
+    show "?f \<in> hom (DirProds (Characters \<circ> Gs) I) (Characters (DirProds Gs I))"
+    proof (intro homI)
+      show "?f x \<in> carrier (Characters (DirProds Gs I))"
+        if x: "x \<in> carrier (DirProds (Characters \<circ> Gs) I)" for x using f_in[OF that] .
+      show "?f (x \<otimes>\<^bsub>DirProds (Characters \<circ> Gs) I\<^esub> y) = ?f x \<otimes>\<^bsub>Characters (DirProds Gs I)\<^esub> ?f y"
+        if "x \<in> carrier (DirProds (Characters \<circ> Gs) I)" "y \<in> carrier (DirProds (Characters \<circ> Gs) I)"
+        for x y
+      proof -
+        have "?f x \<otimes>\<^bsub>Characters (DirProds Gs I)\<^esub> ?f y
+         = (\<lambda>e. if e \<in> carrier (DirProds Gs I) then (\<Prod>i\<in>I. x i (e i)) * (\<Prod>i\<in>I. y i (e i)) else 0)"
+          unfolding Characters_def by auto
+        also have "\<dots> = ?f (x \<otimes>\<^bsub>DirProds (Characters \<circ> Gs) I\<^esub> y)"
+        proof -
+          have "(\<Prod>i\<in>I. x i (e i)) * (\<Prod>i\<in>I. y i (e i))
+              = (\<Prod>i\<in>I. (x \<otimes>\<^bsub>DirProds (Characters \<circ> Gs) I\<^esub> y) i (e i))" for e
+            unfolding DirProds_def Characters_def by (auto simp: prod.distrib)
+          thus ?thesis by presburger
+        qed
+        finally show ?thesis by argo
+      qed
+    qed
+    then interpret fgh: group_hom "DirProds (Characters \<circ> Gs) I" "Characters (DirProds Gs I)" ?f
+      by (unfold_locales, simp)
+    show "bij_betw ?f (carrier (DirProds (Characters \<circ> Gs) I)) (carrier (Characters (DirProds Gs I)))"
+    proof (intro bij_betwI)
+      let ?g = "(\<lambda>c. (\<lambda>i\<in>I. (\<lambda>a. c ((\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i:=a)))))"
+      have allc: "character (Gs i) (?g x i)"
+        if x: "x \<in> carrier (Characters (DirProds Gs I))" and i: "i \<in> I" for x i
+        using DirProds_subchar[OF DP.finite_comm_group_axioms x i assms(3)] .
+      have g_in: "?g x \<in> carrier (DirProds (Characters \<circ> Gs) I)"
+        if x: "x \<in> carrier (Characters (DirProds Gs I))" for x
+        using allc[OF x] unfolding DirProds_def Characters_def characters_def by simp
+      show fi: "?f \<in> carrier (DirProds (Characters \<circ> Gs) I) \<rightarrow> carrier (Characters (DirProds Gs I))"
+        using f_in by fast
+      show gi: "?g \<in> carrier (Characters (DirProds Gs I)) \<rightarrow> carrier (DirProds (Characters \<circ> Gs) I)"
+        using g_in by fast
+      show "?f (?g x) = x" if x: "x \<in> carrier (Characters (DirProds Gs I))" for x
+      proof -
+        from x interpret x: character "DirProds Gs I" x unfolding Characters_def characters_def
+          by auto
+        from f_in[OF g_in[OF x]] interpret character "DirProds Gs I" "?f (?g x)"
+          unfolding Characters_def characters_def by simp
+        have "(\<Prod>i\<in>I. (\<lambda>i\<in>I. \<lambda>a. x ((\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := a))) i (e i)) = x e"
+          if e: "e \<in> carrier (DirProds Gs I)" for e
+        proof -
+          define y where y: "y = (\<lambda>e. if e \<in> carrier (DirProds Gs I)
+                                      then \<Prod>i\<in>I. (\<lambda>i\<in>I. \<lambda>a. x ((\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := a))) i (e i)
+                                      else 0)"
+          from Characters_DirProds_single_prod[OF DP.finite_comm_group_axioms x assms(3)]
+          have "y = x" using y by force
+          hence "y e = x e" by blast
+          thus ?thesis using e unfolding y by argo
+        qed
+        with x.char_eq_0 show ?thesis by force
+      qed
+      show "?g (?f x) = x" if x: "x \<in> carrier (DirProds (Characters \<circ> Gs) I)" for x
+      proof(intro eq_parts_imp_eq[OF g_in[OF f_in[OF x]] x])
+        show "?g (?f x) i = x i" if i: "i\<in>I" for i
+        proof -
+          interpret xi: character "Gs i" "x i"
+            using x i unfolding DirProds_def Characters_def characters_def by auto 
+          have "?g (?f x) i a = x i a" if a: "a\<notin>carrier (Gs i)" for a
+          proof -
+            have "(\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := a) \<notin> carrier (DirProds Gs I)"
+              using a i unfolding DirProds_def PiE_def Pi_def by auto
+            with xi.char_eq_0[OF a] a i show ?thesis by auto
+          qed
+          moreover have "?g (?f x) i a = x i a" if a: "a\<in>carrier (Gs i)" for a
+          proof -
+            have "(\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := a) \<in> carrier (DirProds Gs I)"
+              using a i monoid.one_closed[OF group.is_monoid[OF allg]]
+              unfolding DirProds_def by force
+            moreover have "(\<Prod>j\<in>I. x j (((\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := a)) j)) = x i a"
+            proof -
+              have "(\<Prod>j\<in>I. x j (((\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := a)) j))
+               = x i (((\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := a)) i) * (\<Prod>j\<in>I-{i}. x j (((\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := a)) j))"
+                by (meson assms(3) i prod.remove)
+              moreover have "x j (((\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := a)) j) = 1" if j: "j\<in>I" "j \<noteq> i" for j
+              proof -
+                interpret xj: character "Gs j" "x j"
+                  using j(1) x unfolding DirProds_def Characters_def characters_def by auto
+                show ?thesis using j by auto
+              qed
+              moreover have "x i (((\<lambda>i\<in>I. \<one>\<^bsub>Gs i\<^esub>)(i := a)) i) = x i a" by simp
+              ultimately show ?thesis by auto
+            qed
+            ultimately show ?thesis using a i by simp
+          qed
+          ultimately show ?thesis by blast
+        qed
+      qed
+    qed
+  qed
+  hence "DirProds (Characters \<circ> Gs) I \<cong> Characters (DirProds Gs I)" unfolding is_iso_def by blast
+  moreover have "Characters (DirProds Gs I) \<cong> Characters G"
+    using DP.iso_imp_iso_chars[OF assms(1) is_group] .
+  ultimately show ?thesis using iso_trans by blast
+qed
+
+text \<open>As thus both the group and its character group can be decomposed into the same cyclic factors,
+the isomorphism follows for any finite abelian group.\<close>
+
+theorem (in finite_comm_group) Characters_iso:
+  shows "G \<cong> Characters G"
+proof -
+  from cyclic_product obtain ns
+    where ns: "DirProds (\<lambda>n. Z (ns ! n)) {..<length ns} \<cong> G" "\<forall>n\<in>set ns. n \<noteq> 0" .
+  interpret DP: group "DirProds (\<lambda>n. Z (ns ! n)) {..<length ns}"
+    by (intro DirProds_is_group, auto)
+  have "G \<cong> DirProds (\<lambda>n. Z (ns ! n)) {..<length ns}" using DP.iso_sym[OF ns(1)] .
+  moreover have "DirProds (Characters \<circ> (\<lambda>n. Z (ns ! n))) {..<length ns} \<cong> Characters G"
+    by (intro Characters_DirProds_iso[OF ns(1) DirProds_is_group], auto)
+  moreover have "DirProds (\<lambda>n. Z (ns ! n)) {..<length ns}
+               \<cong> DirProds (Characters \<circ> (\<lambda>n. Z (ns ! n))) {..<length ns}"
+  proof (intro DirProds_iso1)
+    fix i assume i: "i \<in> {..<length ns}"
+    obtain a where "cyclic_group (Z (ns!i)) a" using Zn_cyclic_group .
+    then interpret Zi: cyclic_group "Z (ns!i)" a .
+    interpret Zi: finite_cyclic_group "Z (ns!i)" a
+    proof
+      have "order (Z (ns ! i)) \<noteq> 0" using ns(2) i Zn_order by simp
+      thus "finite (carrier (Z (ns ! i)))" unfolding order_def by (simp add: card_eq_0_iff)
+    qed
+    show "Group.group ((Characters \<circ> (\<lambda>n. Z (ns ! n))) i)"
+         "Group.group (Z (ns ! i))" "Z (ns ! i) \<cong> (Characters \<circ> (\<lambda>n. Z (ns ! n))) i"
+      using Zi.Characters_iso Zi.finite_comm_group_Characters comm_group_def finite_comm_group_def
+      by auto
+  qed
+  ultimately show ?thesis by (auto elim: iso_trans)
+qed
+
+text \<open>Hence, the orders are also equal.\<close>
+
+corollary (in finite_comm_group) order_Characters:
+  "order (Characters G) = order G"
+  using iso_same_card[OF Characters_iso] unfolding order_def by argo
+
+corollary (in finite_comm_group) card_characters: "card (characters G) = order G"
+  using order_Characters unfolding order_def Characters_def by simp
 
 subsection \<open>Non-trivial facts about characters\<close>
 
-context finite_comm_group
-begin
-
-text \<open>
-  The following theorem is a very central one. It shows that any character on a subgroup \<open>H\<close> can
-  be extended to a character on the full group in exactly $[G : H]$ ways.
-
-  The proof is by induction; we start with \<open>H\<close> and then successively adjoin elements until we
-  have reached \<open>G\<close>. As we showed before, when we lift a character from \<open>H\<close> to $H_x$, we have
-  \<open>n\<close> choices to do so, where \<open>n\<close> is the indicator of \<open>x\<close> in \<open>H\<close>. Since $|H_x| = n |H|$, the
-  induction step is valid.
-\<close>
-theorem card_character_extensions:
-  assumes "subgroup H G" "character (G\<lparr>carrier := H\<rparr>) \<chi>"
-  shows   "card {\<chi>'\<in>characters G. \<forall>x\<in>H. \<chi>' x = \<chi> x} * card H = order G"
-  using assms
-proof (induction rule: subgroup_adjoin_induct)
-  case (base )
-  have "{\<chi>' \<in> characters (G\<lparr>carrier := H\<rparr>). \<forall>x\<in>H. \<chi>' x = \<chi> x} = {\<chi>}"
-    using base by (auto simp: fun_eq_iff characters_def intro: character_ext)
-  thus ?case using base by (simp add: order_def)
-next
-  case (adjoin H' a )
-  interpret H': subgroup H' G by fact
-  interpret H': finite_comm_group "G\<lparr>carrier := H'\<rparr>"
-    by (rule subgroup_imp_finite_comm_group) fact
-  interpret H': finite_comm_group_adjoin G H' a
-    using adjoin.hyps by unfold_locales auto
-
-  define h where "h = subgroup_indicator G H' a"
-  from adjoin have [simp]: "h > 0" unfolding h_def by (intro subgroup_indicator_pos) auto
-  define c where "c = a [^] h"
-  from adjoin have [simp]: "c \<in> H'"
-    by (auto simp: c_def h_def pow_subgroup_indicator)
+text \<open>We characterize the character group of a quotient group as the group of characters that map
+all elements of the subgroup onto $1$.\<close>
 
-  define C where "C = (\<lambda>H'. {\<chi>'. \<chi>' \<in> characters (G\<lparr>carrier := H'\<rparr>) \<and> (\<forall>x\<in>H. \<chi>' x = \<chi> x)})"
-  define I where "I = (\<lambda>\<chi>. {z::complex. z ^ h = \<chi> c})"
-  have [simp]: "finite (C H')"
-    by (rule finite_subset[OF _ H'.finite_characters]) (auto simp: C_def)
+lemma (in finite_comm_group) iso_Characters_FactGroup:
+  assumes H: "subgroup H G"
+  shows "(\<lambda>\<chi> x. if x \<in> carrier G then \<chi> (H #> x) else 0) \<in>
+           iso (Characters (G Mod H)) ((Characters G)\<lparr>carrier := {\<chi>\<in>characters G. \<forall>x\<in>H. \<chi> x = 1}\<rparr>)"
+proof -
+  interpret H: normal H G using subgroup_imp_normal[OF H] .
+  interpret Chars: finite_comm_group "Characters G"
+    by (rule finite_comm_group_Characters)
+  interpret Fact: comm_group "G Mod H"
+    by (simp add: H.subgroup_axioms comm_group.abelian_FactGroup comm_group_axioms)
+  interpret Fact: finite_comm_group "G Mod H"
+    by unfold_locales (auto simp: carrier_FactGroup)
 
-  (* TODO: extract lemma *)
-  have "bij_betw H'.lift_character (SIGMA \<chi>:C H'. I \<chi>) (C (adjoin G H' a))"
-  proof (rule bij_betwI)
-    show "H'.lift_character \<in> Sigma (C H') I \<rightarrow> C (adjoin G H' a)"
-    proof safe
-      fix \<chi> z assume *: "\<chi> \<in> C H'" "z \<in> I \<chi>"
-      have "\<forall>x\<in>H. H'.lift_character (\<chi>, z) x = \<chi> x"
-        using * adjoin.hyps by auto
-      with * show "H'.lift_character (\<chi>, z) \<in> C (adjoin G H' a)"
-        using H'.lift_character[of \<chi> z]
-        by (auto simp: C_def I_def h_def c_def characters_def)
-    qed
+  define C :: "('a \<Rightarrow> complex) set" where "C = {\<chi>\<in>characters G. \<forall>x\<in>H. \<chi> x = 1}"
+  interpret C: subgroup C "Characters G"
+  proof (unfold_locales, goal_cases)
+    case 1
+    thus ?case
+      by (auto simp: C_def one_Characters mult_Characters carrier_Characters characters_def)
   next
-    show "(\<lambda>\<chi>. (\<lambda>x. if x \<in> H' then \<chi> x else 0, \<chi> a)) \<in> C (adjoin G H' a) \<rightarrow> Sigma (C H') I"
-    proof safe
-      fix \<chi> assume \<chi>: "\<chi> \<in> C (adjoin G H' a)"
-      thus "(\<lambda>xa. if xa \<in> H' then \<chi> xa else 0) \<in> C H'"
-        using H'.lower_character[of \<chi>] adjoin.prems adjoin.hyps
-        by (auto simp: C_def characters_def character.char_eq_0)
-      have "\<chi> (a [^]\<^bsub>G\<lparr>carrier := adjoin G H' a\<rparr>\<^esub> subgroup_indicator (G\<lparr>carrier := adjoin G H' a\<rparr>) H' a) =
-              \<chi> a ^ subgroup_indicator (G\<lparr>carrier := adjoin G H' a\<rparr>) H' a"
-        using \<chi> adjoin.prems adjoin.hyps
-        by (intro character.char_power) (auto simp: C_def characters_def adjoined_in_adjoin)
-      hence "\<chi> (a [^] h) = \<chi> a ^ subgroup_indicator G H' a"
-        by (simp add: nat_pow_consistent [symmetric] h_def)
-      with \<chi> show "\<chi> a \<in> I (\<lambda>xa. if xa \<in> H' then \<chi> xa else 0)"
-        using adjoin.hyps adjoin.prems
-        by (auto simp: I_def C_def characters_def character.char_power character.char_eq_0
-                       pow_subgroup_indicator h_def c_def)
-    qed
+    case 2
+    thus ?case
+      by (auto simp: C_def one_Characters mult_Characters carrier_Characters characters_def)
   next
-    fix \<chi>z assume *: "\<chi>z \<in> (SIGMA \<chi>:C H'. I \<chi>)"
-    obtain \<chi> z where [simp]: "\<chi>z = (\<chi>, z)" by (cases \<chi>z)
-    from * show "(\<lambda>xa. if xa \<in> H' then H'.lift_character \<chi>z xa else 0, H'.lift_character \<chi>z a) = \<chi>z"
-      using H'.lower_character_lift_character[of \<chi> z] by (auto simp: C_def cong: if_cong)
+    case 3
+    thus ?case
+      by (auto simp: C_def one_Characters mult_Characters
+                     carrier_Characters characters_def principal_char_def)
   next
-    fix \<chi> assume "\<chi> \<in> C (adjoin G H' a)"
-    thus "H'.lift_character (\<lambda>x. if x \<in> H' then \<chi> x else 0, \<chi> a) = \<chi>"
-      using H'.lift_character_lower_character[of \<chi>] by (auto simp: C_def)
+    case (4 \<chi>)
+    hence "inv\<^bsub>Characters G\<^esub> \<chi> = inv_character \<chi>"
+      by (subst inv_Characters') (auto simp: C_def carrier_Characters)
+    moreover have "inv_character \<chi> \<in> characters G"
+      using 4 by (auto simp: C_def characters_def)
+    moreover have "\<forall>x\<in>H. inv_character \<chi> x = 1"
+      using 4 by (auto simp: C_def inv_character_def)
+    ultimately show ?case
+      by (auto simp: C_def)
   qed
 
-  hence "card (SIGMA \<chi>:C H'. I \<chi>) = card (C (adjoin G H' a))"
-    by (rule bij_betw_same_card)
-  also have "card (SIGMA \<chi>:C H'. I \<chi>) = (\<Sum>a\<in>C H'. card (I a))"
-    by (intro card_SigmaI) (auto simp: I_def)
-  also have "\<dots> = (\<Sum>a\<in>C H'. h)"
-  proof (intro sum.cong refl, goal_cases)
-    case (1 \<chi>)
-    then interpret character "G\<lparr>carrier := H'\<rparr>" \<chi> by (simp add: characters_def C_def)
-    have "\<chi> c \<noteq> 0"
-      by (subst char_eq_0_iff) (auto simp: c_def h_def intro!: pow_subgroup_indicator adjoin)
-    thus ?case by (simp add: I_def card_nth_roots)
+  define f :: "('a set \<Rightarrow> complex) \<Rightarrow> ('a \<Rightarrow> complex)"
+    where "f = (\<lambda>\<chi> x. if x \<in> carrier G then \<chi> (H #> x) else 0)"
+
+  have [intro]: "character G (f \<chi>)" if "character (G Mod H) \<chi>" for \<chi>
+  proof -
+    interpret character "G Mod H" \<chi> by fact
+    show ?thesis
+    proof (unfold_locales, goal_cases)
+      case 1
+      thus ?case by (auto simp: f_def char_eq_0_iff carrier_FactGroup)
+    next
+      case (2 x)
+      thus ?case by (auto simp: f_def)
+    next
+      case (3 x y)
+      have "\<chi> (H #> x) * \<chi> (H #> y) = \<chi> ((H #> x) \<otimes>\<^bsub>G Mod H\<^esub> (H #> y))"
+        using 3 by (intro char_mult [symmetric]) (auto simp: carrier_FactGroup)
+      also have "(H #> x) \<otimes>\<^bsub>G Mod H\<^esub> (H #> y) = H #> (x \<otimes> y)"
+        using 3 by (simp add: H.rcos_sum)
+      finally show ?case
+        using 3 by (simp add: f_def)
+    qed
   qed
-  also have "\<dots> = h * card (C H')" by simp
-  finally have "card (C (adjoin G H' a)) * card H = h * (card (C H') * card H)"
-    by simp
-  also have "card (C H') * card H = card H'"
-    unfolding C_def using adjoin.prems by (subst adjoin.IH) (auto simp: order_def)
-  also have "h * card H' = card (adjoin G H' a)"
-    using adjoin.hyps by (subst card_adjoin) (auto simp: h_def)
-  also have "\<dots> = order (G\<lparr>carrier := adjoin G H' a\<rparr>)"
-    by (simp add: order_def)
-  finally show ?case by (simp add: C_def)
+
+  have [intro]: "f \<chi> \<in> C" if "character (G Mod H) \<chi>" for \<chi>
+  proof -
+    interpret \<chi>: character "G Mod H" \<chi>
+      by fact
+    have "character G (f \<chi>)"
+      using \<chi>.character_axioms by auto
+    moreover have "\<chi> (H #> x) = 1" if "x \<in> H" for x
+      using that H.rcos_const \<chi>.char_one by force
+    ultimately show ?thesis
+      by (auto simp: carrier_Characters C_def characters_def f_def)
+  qed
+
+  show "f \<in> iso (Characters (G Mod H)) ((Characters G)\<lparr>carrier := C\<rparr>)"
+  proof (rule isoI)
+    show "f \<in> hom (Characters (G Mod H)) (Characters G\<lparr>carrier := C\<rparr>)"
+    proof (rule homI, goal_cases)
+      case (1 \<chi>)
+      thus ?case
+        by (auto simp: carrier_Characters characters_def)
+    qed (auto simp: f_def carrier_Characters fun_eq_iff mult_Characters)
+  next
+    have "bij_betw f (characters (G Mod H)) C"
+      unfolding bij_betw_def
+    proof
+      show inj: "inj_on f (characters (G Mod H))"
+      proof (rule inj_onI, goal_cases)
+        case (1 \<chi>1 \<chi>2)
+        interpret \<chi>1: character "G Mod H" \<chi>1
+          using 1 by (auto simp: characters_def)
+        interpret \<chi>2: character "G Mod H" \<chi>2
+          using 1 by (auto simp: characters_def)
+
+        have "\<chi>1 H' = \<chi>2 H'" for H'
+        proof (cases "H' \<in> carrier (G Mod H)")
+          case False
+          thus ?thesis by (simp add: \<chi>1.char_eq_0 \<chi>2.char_eq_0)
+        next
+          case True
+          then obtain x where x: "x \<in> carrier G" "H' = H #> x"
+            by (auto simp: carrier_FactGroup)
+          from 1 have "f \<chi>1 x = f \<chi>2 x"
+            by simp
+          with x show ?thesis
+            by (auto simp: f_def)
+        qed
+        thus "\<chi>1 = \<chi>2" by force
+      qed
+    
+      have "f ` characters (G Mod H) \<subseteq> C"
+        by (auto simp: characters_def)
+      moreover have "C \<subseteq> f ` characters (G Mod H)"
+      proof safe
+        fix \<chi> assume \<chi>: "\<chi> \<in> C"
+        from \<chi> interpret character G \<chi>
+          by (auto simp: C_def characters_def)
+        have [simp]: "\<chi> x = 1" if "x \<in> H" for x
+          using \<chi> that by (auto simp: C_def)
+
+        have "\<forall>H'\<in>carrier (G Mod H). \<exists>x\<in>carrier G. H' = H #> x"
+          by (auto simp: carrier_FactGroup)
+        then obtain h where h: "h H' \<in> carrier G" "H' = H #> h H'" if "H' \<in> carrier (G Mod H)" for H'
+          by metis
+        define \<chi>' where "\<chi>' = (\<lambda>H'. if H' \<in> carrier (G Mod H) then \<chi> (h H') else 0)"
+
+        have \<chi>_cong: "\<chi> x = \<chi> y" if "H #> x = H #> y" "x \<in> carrier G" "y \<in> carrier G" for x y
+        proof -
+          have "x \<in> H #> x"
+            by (simp add: H.subgroup_axioms rcos_self that(2))
+          also have "\<dots> = H #> y"
+            by fact
+          finally obtain z where z: "z \<in> H" "x = z \<otimes> y"
+            unfolding r_coset_def by auto
+          thus ?thesis
+            using z H.subset that by simp
+        qed
+
+        have "character (G Mod H) \<chi>'"
+        proof (unfold_locales, goal_cases)
+          case 1
+          have H: "H \<in> carrier (G Mod H)"
+            using Fact.one_closed unfolding one_FactGroup .
+          with h[of H] have "h H \<in> carrier G"
+            by blast
+          thus ?case using H
+            by (auto simp: char_eq_0_iff \<chi>'_def)
+        next
+          case (2 H')
+          thus ?case by (auto simp: \<chi>'_def)
+        next
+          case (3 H1 H2)
+          from 3 have H12: "H1 <#> H2 \<in> carrier (G Mod H)"
+            using Fact.m_closed by force
+          have "\<chi> (h (H1 <#> H2)) = \<chi> (h H1 \<otimes> h H2)"
+          proof (rule \<chi>_cong)
+            show "H #> h (H1 <#> H2) = H #> (h H1 \<otimes> h H2)"
+              by (metis "3" H.rcos_sum H12 h)
+          qed (use 3 h[of H1] h[of H2] h[OF H12] in auto)
+          thus ?case
+            using 3 H12 h[of H1] h[of H2] by (auto simp: \<chi>'_def)
+        qed
+
+        moreover have "f \<chi>' x = \<chi> x" for x
+        proof (cases "x \<in> carrier G")
+          case False
+          thus ?thesis
+            by (auto simp: f_def \<chi>'_def char_eq_0_iff)
+        next
+          case True
+          hence *: "H #> x \<in> carrier (G Mod H)"
+            by (auto simp: carrier_FactGroup)
+          have "\<chi> (h (H #> x)) = \<chi> x"
+            using True * h[of "H #> x"] by (intro \<chi>_cong) auto
+          thus ?thesis
+            using True * by (auto simp: f_def fun_eq_iff \<chi>'_def)
+        qed
+        hence "f \<chi>' = \<chi>" by force
+
+        ultimately show "\<chi> \<in> f ` characters (G Mod H)"
+          unfolding characters_def by blast
+      qed
+
+      ultimately show "f ` characters (G Mod H) = C"
+        by blast
+
+    qed
+    thus "bij_betw f (carrier (Characters (G Mod H))) (carrier (Characters G\<lparr>carrier := C\<rparr>))"
+      by (simp add: carrier_Characters)
+  qed 
+qed
+
+lemma (in finite_comm_group) is_iso_Characters_FactGroup:
+  assumes H: "subgroup H G"
+  shows "Characters (G Mod H) \<cong> (Characters G)\<lparr>carrier := {\<chi>\<in>characters G. \<forall>x\<in>H. \<chi> x = 1}\<rparr>"
+  using iso_Characters_FactGroup[OF assms] unfolding is_iso_def by blast
+
+text \<open>In order to derive the number of extensions a character on a subgroup has to the entire group,
+we introduce the group homomorphism \<open>restrict_char\<close> that restricts a character to a given subgroup \<open>H\<close>.\<close>
+
+definition restrict_char::"'a set \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> ('a \<Rightarrow> complex) " where
+"restrict_char H \<chi> = (\<lambda>e. if e\<in>H then \<chi> e else 0)"
+
+lemma (in finite_comm_group) restrict_char_hom:
+  assumes "subgroup H G"
+  shows "group_hom (Characters G) (Characters (G\<lparr>carrier := H\<rparr>)) (restrict_char H)"
+proof -
+  let ?CG = "Characters G"
+  let ?H = "G\<lparr>carrier := H\<rparr>"
+  let ?CH = "Characters ?H" 
+  interpret H: subgroup H G by fact
+  interpret H: finite_comm_group ?H by (simp add: assms subgroup_imp_finite_comm_group)
+  interpret CG: finite_comm_group ?CG using finite_comm_group_Characters .
+  interpret CH: finite_comm_group ?CH using H.finite_comm_group_Characters .
+  show ?thesis
+  proof(unfold_locales, intro homI)
+    show "restrict_char H x \<in> carrier ?CH" if x: "x \<in> carrier ?CG" for x
+    proof -
+      interpret xc: character G x using x unfolding Characters_def characters_def by simp
+      have "character ?H (restrict_char H x)"
+        by (unfold restrict_char_def, unfold_locales, auto)
+      thus ?thesis unfolding Characters_def characters_def by simp
+    qed
+    show "restrict_char H (x \<otimes>\<^bsub>?CG\<^esub> y) = restrict_char H x \<otimes>\<^bsub>?CH\<^esub> restrict_char H y"
+      if x: "x \<in> carrier ?CG" and y: "y \<in> carrier ?CG" for x y
+    proof -
+      interpret xc: character G x using x unfolding Characters_def characters_def by simp
+      interpret yc: character G y using y unfolding Characters_def characters_def by simp
+      show ?thesis unfolding Characters_def restrict_char_def by auto
+    qed
+  qed
+qed
+
+text \<open>The kernel is just the set of the characters that are $1$ on all of \<open>H\<close>.\<close>
+
+lemma (in finite_comm_group) restrict_char_kernel:
+  assumes "subgroup H G"
+  shows "kernel (Characters G) (Characters (G\<lparr>carrier := H\<rparr>)) (restrict_char H)
+       = {\<chi>\<in>characters G. \<forall>x\<in>H. \<chi> x = 1}"
+  by (unfold restrict_char_def kernel_def one_Characters
+             carrier_Characters principal_char_def characters_def, simp, metis)
+
+text \<open>Also, all of the characters on the subgroup are the image of some character on the whole group.\<close>
+
+lemma (in finite_comm_group) restrict_char_image:
+  assumes "subgroup H G"
+  shows "restrict_char H ` (carrier (Characters G)) = carrier (Characters (G\<lparr>carrier := H\<rparr>))"
+proof -
+  interpret H: subgroup H G by fact
+  interpret H: finite_comm_group "G\<lparr>carrier := H\<rparr>" using subgroup_imp_finite_comm_group[OF assms] .
+  interpret r: group_hom "Characters G" "Characters (G\<lparr>carrier := H\<rparr>)" "restrict_char H"
+    using restrict_char_hom[OF assms] .
+  interpret Mod: finite_comm_group "G Mod H" using finite_comm_FactGroup[OF assms] .
+  interpret CG: finite_comm_group "Characters G" using finite_comm_group_Characters .
+  have c1: "order (Characters (G\<lparr>carrier := H\<rparr>)) = card H" using H.order_Characters
+    unfolding order_def by simp
+  
+  have "card H * card (kernel (Characters G) (Characters (G\<lparr>carrier := H\<rparr>)) (restrict_char H))
+      = order G"
+    using restrict_char_kernel[OF assms] iso_same_card[OF is_iso_Characters_FactGroup[OF assms]]
+          Mod.order_Characters lagrange[OF assms] unfolding order_def FactGroup_def
+    by (force simp: algebra_simps)
+  moreover have "card (kernel (Characters G) (Characters (G\<lparr>carrier := H\<rparr>)) (restrict_char H)) \<noteq> 0"
+    using r.one_in_kernel unfolding kernel_def CG.fin by auto
+  ultimately have c2: "card H = card (restrict_char H ` carrier (Characters G))"
+    using r.image_kernel_product[unfolded order_Characters] by (metis mult_right_cancel)
+
+  have "restrict_char H ` (carrier (Characters G)) \<subseteq> carrier (Characters (G\<lparr>carrier := H\<rparr>))"
+    by auto
+  with c2 H.fin show ?thesis
+    by (auto, metis H.finite_imp_card_positive c1 card_subset_eq fin_gen
+                    order_def r.H.order_gt_0_iff_finite)
 qed
 
 text \<open>
-  By taking \<open>H\<close> to be the trivial subgroup, we obtain that the number of characters
-  on \<open>G\<close> is precisely the order of \<open>G\<close> itself, i.\,e.\ $|\widehat{G}|=|G|$.
-\<close>
-corollary card_characters: "card (characters G) = order G"
-proof -
-  define \<chi> where "\<chi> = principal_char (G\<lparr>carrier := {\<one>}\<rparr>)"
-  interpret triv: subgroup "{\<one>}"
-    by standard auto
-  interpret triv: finite_comm_group "G\<lparr>carrier := {\<one>}\<rparr>"
-    by (rule subgroup_imp_finite_comm_group) (rule triv.is_subgroup)
-  
-  have "card {\<chi>'\<in>characters G. \<forall>x\<in>{\<one>}. \<chi>' x = \<chi> x} * card {\<one>} = order G"
-    unfolding \<chi>_def
-    by (intro card_character_extensions triv.is_subgroup triv.character_principal)
-  also have "{\<chi>'\<in>characters G. \<forall>x\<in>{\<one>}. \<chi>' x = \<chi> x} = characters G"
-    by (auto simp: characters_def character.char_one principal_char_def \<chi>_def)
-  finally show ?thesis by simp
-qed
-
-lemma order_Characters [simp]: "order (Characters G) = order G"
-  by (simp add: order_def card_characters carrier_Characters)
-
-text \<open>
-  It also follows as a simple corollary that any character on \<open>H\<close> \<^emph>\<open>can\<close> be extended
+  It follows that any character on \<open>H\<close> can be extended
   to a character on \<open>G\<close>.
 \<close>
-corollary character_extension_exists:
+
+lemma (in finite_comm_group) character_extension_exists:
   assumes "subgroup H G" "character (G\<lparr>carrier := H\<rparr>) \<chi>"
   obtains \<chi>' where "character G \<chi>'" and "\<And>x. x \<in> H \<Longrightarrow> \<chi>' x = \<chi> x"
 proof -
-  have "card {\<chi>'\<in>characters G. \<forall>x\<in>H. \<chi>' x = \<chi> x} * card H = order G"
-    by (intro card_character_extensions assms)
-  hence "card {\<chi>'\<in>characters G. \<forall>x\<in>H. \<chi>' x = \<chi> x} \<noteq> 0"
-    using order_gt_0 by (intro notI) auto
-  hence "{\<chi>'\<in>characters G. \<forall>x\<in>H. \<chi>' x = \<chi> x} \<noteq> {}"
-    by (intro notI) simp
-  then obtain \<chi>' where "character G \<chi>'" and "\<And>x. x \<in> H \<Longrightarrow> \<chi>' x = \<chi> x"
-    unfolding characters_def by blast
-  thus ?thesis using that[of \<chi>'] by blast
+  from restrict_char_image[OF assms(1)] assms(2) obtain \<chi>'
+    where chi': "restrict_char H \<chi>' = \<chi>" "character G \<chi>'"
+    by (force simp: carrier_Characters characters_def)
+  thus ?thesis using that restrict_char_def by metis
+qed
+
+text \<open>For two characters on a group \<open>G\<close> the number of characters on subgroup \<open>H\<close> that share the
+values with them is the same for both.\<close>
+
+lemma (in finite_comm_group) character_restrict_card: 
+  assumes "subgroup H G" "character G a" "character G b"
+  shows   "card {\<chi>'\<in>characters G. \<forall>x\<in>H. \<chi>' x = a x} = card {\<chi>'\<in>characters G. \<forall>x\<in>H. \<chi>' x = b x}"
+proof -
+  interpret H: subgroup H G by fact
+  interpret H: finite_comm_group "G\<lparr>carrier := H\<rparr>" using assms(1)
+    by (simp add: subgroup_imp_finite_comm_group)
+  interpret CG: finite_comm_group "Characters G" using finite_comm_group_Characters .
+  interpret a: character G a by fact
+  interpret b: character G b by fact
+  have ac: "a \<in> carrier (Characters G)" unfolding Characters_def characters_def using assms by simp
+  have bc: "b \<in> carrier (Characters G)" unfolding Characters_def characters_def using assms by simp
+  define f where f: "f = (\<lambda>c. b \<otimes>\<^bsub>Characters G\<^esub> inv\<^bsub>Characters G\<^esub> a \<otimes>\<^bsub>Characters G\<^esub> c)"
+  define g where g: "g = (\<lambda>c. a \<otimes>\<^bsub>Characters G\<^esub> inv\<^bsub>Characters G\<^esub> b \<otimes>\<^bsub>Characters G\<^esub> c)"
+  let ?A = "{\<chi>'\<in>characters G. \<forall>x\<in>H. \<chi>' x = a x}"
+  let ?B = "{\<chi>'\<in>characters G. \<forall>x\<in>H. \<chi>' x = b x}"
+  have "bij_betw f ?A ?B"
+  proof(intro bij_betwI[of _ _ _ g])
+    show "f \<in> ?A \<rightarrow> ?B"
+    proof
+      show "f x \<in> ?B" if x: "x \<in> ?A" for x
+      proof -
+        interpret xc: character G x using x unfolding characters_def by blast
+        have xc: "x \<in> carrier (Characters G)" using x unfolding Characters_def by simp
+        have "f x y = b y" if y: "y \<in> H" for y
+        proof -
+          have "(inv\<^bsub>Characters G\<^esub> a) y * a y =  1"
+            by (simp add: a.inv_Characters a.mult_inv_character mult.commute principal_char_def y)
+          thus ?thesis unfolding f mult_Characters using x y by fastforce
+        qed
+        thus "f x \<in> ?B" unfolding f carrier_Characters[symmetric] using ac bc xc by blast
+      qed
+    qed
+    show "g \<in> ?B \<rightarrow> ?A"
+    proof
+      show "g x \<in> ?A" if x: "x \<in> ?B" for x
+      proof -
+        interpret xc: character G x using x unfolding characters_def by blast
+        have xc: "x \<in> carrier (Characters G)" using x unfolding Characters_def by simp
+        have "g x y = a y" if y: "y \<in> H" for y
+        proof -
+          have "(inv\<^bsub>Characters G\<^esub> b) y * x y = 1" using x y
+            by (simp add: b.inv_Characters b.mult_inv_character mult.commute principal_char_def)
+          thus ?thesis unfolding g mult_Characters by simp
+        qed
+        thus "g x \<in> ?A" unfolding g carrier_Characters[symmetric] using ac bc xc by blast
+      qed
+    qed
+    show "g (f x) = x" if x: "x \<in> ?A" for x
+    proof -
+      have xc: "x \<in> carrier (Characters G)" using x unfolding Characters_def by force
+      with ac bc show ?thesis unfolding f g
+        by (auto simp: CG.m_assoc[symmetric],
+            metis CG.inv_closed CG.inv_comm CG.l_inv CG.m_assoc CG.r_one)
+    qed
+    show "f (g x) = x" if x: "x \<in> ?B" for x
+    proof -
+      have xc: "x \<in> carrier (Characters G)" using x unfolding Characters_def by force
+      with ac bc show ?thesis unfolding f g
+        by (auto simp: CG.m_assoc[symmetric],
+            metis CG.inv_closed CG.inv_comm CG.l_inv CG.m_assoc CG.r_one)
+    qed
+  qed
+  thus ?thesis using bij_betw_same_card by blast
+qed
+
+text \<open>These lemmas allow to show that the number of extensions of a character on \<open>H\<close> to a
+character on \<open>G\<close> is just $|G|/|H|$.\<close>
+
+theorem (in finite_comm_group) card_character_extensions:
+  assumes "subgroup H G" "character (G\<lparr>carrier := H\<rparr>) \<chi>"
+  shows   "card {\<chi>'\<in>characters G. \<forall>x\<in>H. \<chi>' x = \<chi> x} * card H = order G"
+proof -
+  interpret H: subgroup H G by fact
+  interpret H: finite_comm_group "G\<lparr>carrier := H\<rparr>"
+    using subgroup_imp_finite_comm_group[OF assms(1)] .
+  interpret chi: character "G\<lparr>carrier := H\<rparr>" \<chi> by fact
+  interpret C: finite_comm_group "Characters G" using finite_comm_group_Characters .
+  interpret Mod: finite_comm_group "G Mod H" using finite_comm_FactGroup[OF assms(1)] .
+  obtain a where a: "a \<in> carrier (Characters G)" "restrict_char H a = \<chi>"
+  proof -
+    have "\<exists>a\<in>carrier (Characters G). restrict_char H a = \<chi>"
+      using restrict_char_image[OF assms(1)] assms(2)
+      unfolding carrier_Characters characters_def image_def by force
+    thus ?thesis using that by blast
+  qed
+  show ?thesis
+  proof -
+    have p: "{\<chi>\<in>characters G. \<forall>x\<in>H. \<chi> x = 1} = {\<chi>\<in>characters G. \<forall>x\<in>H. \<chi> x = principal_char G x}"
+      unfolding principal_char_def by force
+    have ac: "{\<chi>'\<in>characters G. \<forall>x\<in>H. \<chi>' x = \<chi> x} = {\<chi>'\<in>characters G. \<forall>x\<in>H. \<chi>' x = a x}"
+      using a(2) unfolding restrict_char_def by force
+    have "card {\<chi>\<in>characters G. \<forall>x\<in>H. \<chi> x = 1} = card {\<chi>'\<in>characters G. \<forall>x\<in>H. \<chi>' x = \<chi> x}"
+      by (unfold ac p; intro character_restrict_card[OF assms(1)],
+          use a[unfolded Characters_def characters_def] in auto)
+    moreover have "card {\<chi>\<in>characters G. \<forall>x\<in>H. \<chi> x = 1} = card (carrier (G Mod H))"
+      using iso_same_card[OF is_iso_Characters_FactGroup[OF assms(1)]]
+            Mod.order_Characters[unfolded order_def] by force
+    moreover have "card (carrier (G Mod H)) * card H = order G"
+      using lagrange[OF assms(1)] unfolding FactGroup_def by simp
+    ultimately show ?thesis by argo
+  qed
 qed
 
 text \<open>
   Lastly, we can also show that for each $x\in H$ of order $n > 1$ and each \<open>n\<close>-th root of
   unity \<open>z\<close>, there exists a character \<open>\<chi>\<close> on \<open>G\<close> such that $\chi(x) = z$.
 \<close>
-corollary character_with_value_exists:
+
+lemma (in group) powi_get_exp_self:
+  fixes z::complex
+  assumes "z ^ n = 1" "x \<in> carrier G" "ord x = n" "n > 1"
+  shows "z powi get_exp x x = z"
+proof -
+  from assms have ngt0: "n > 0" by simp
+  from powi_mod[OF assms(1) ngt0, of "get_exp x x"] get_exp_self[OF assms(2), unfolded assms(3)]
+  have "z powi get_exp x x = z powi (1 mod int n)" by argo    
+  also have "\<dots> = z" using assms(4) by simp
+  finally show ?thesis .
+qed
+
+corollary (in finite_comm_group) character_with_value_exists:
   assumes "x \<in> carrier G" and "x \<noteq> \<one>" and "z ^ ord x = 1"
   obtains \<chi> where "character G \<chi>" and "\<chi> x = z"
 proof -
-  define triv where "triv = G\<lparr>carrier := {\<one>}\<rparr>"
-  interpret triv: subgroup "{\<one>}"
-    by standard auto
-  interpret triv: finite_comm_group "G\<lparr>carrier := {\<one>}\<rparr>"
-    by (rule subgroup_imp_finite_comm_group) (rule triv.is_subgroup)
-  interpret H: finite_comm_group_adjoin G "{\<one>}" x
-    using assms by unfold_locales auto
-
-  define h where "h = subgroup_indicator G {\<one>} x"
-  have x_pow_h: "x [^] h = \<one>"
-    using pow_subgroup_indicator[OF triv.is_subgroup assms(1)] by (simp add: h_def)
-  have "h > 0"
-    using subgroup_indicator_pos[OF triv.is_subgroup assms(1)] by (simp add: h_def)
-  have [simp]: "ord x = h"
-    using x_pow_h triv.is_subgroup assms \<open>h > 0\<close> unfolding h_def
-    by (intro antisym subgroup_indicator_le_ord ord_min) auto
-
-  define \<chi> where "\<chi> = principal_char triv"
-  define \<chi>' where "\<chi>' = H.lift_character (\<chi>, z)"
-  have "subgroup (adjoin G {\<one>} x) G"
-    by (intro adjoin_subgroup triv.is_subgroup assms)
-  moreover have \<chi>': "character (G\<lparr>carrier := adjoin G {\<one>} x\<rparr>) \<chi>'"
-    using H.lift_character[of \<chi> z] triv.character_principal assms x_pow_h
-    by (auto simp: \<chi>'_def \<chi>_def principal_char_def triv_def h_def)
-  ultimately obtain \<chi>'' where \<chi>'': "character G \<chi>''" "\<And>y. y \<in> adjoin G {\<one>} x \<Longrightarrow> \<chi>'' y = \<chi>' y"
-    by (erule character_extension_exists)
-  moreover {
-    have "\<chi>'' x = \<chi>' x"
-      using \<chi>''(2)[of x] assms triv.is_subgroup by (auto simp: adjoined_in_adjoin)
-    also have "\<chi>' x = z"
-      unfolding \<chi>'_def by (subst H.lift_character_adjoined) (simp_all add: \<chi>_def triv_def)
-    finally have "\<chi>'' x = z" .
-  }
-  ultimately show ?thesis using that[of \<chi>''] by blast
+  interpret H: subgroup "generate G {x}" G using generate_is_subgroup assms(1) by simp
+  interpret H: finite_comm_group "G\<lparr>carrier := generate G {x}\<rparr>"
+    using subgroup_imp_finite_comm_group[OF H.subgroup_axioms] . 
+  interpret H: finite_cyclic_group "G\<lparr>carrier := generate G {x}\<rparr>" x
+  proof(unfold finite_cyclic_group_def, safe)
+    show "finite_group (G\<lparr>carrier := generate G {x}\<rparr>)" by unfold_locales
+    show "cyclic_group (G\<lparr>carrier := generate G {x}\<rparr>) x"
+    proof(intro H.cyclic_groupI0)
+      show "x \<in> carrier (G\<lparr>carrier := generate G {x}\<rparr>)" using generate.incl[of x "{x}" G] by simp
+      show "carrier (G\<lparr>carrier := generate G {x}\<rparr>) = generate (G\<lparr>carrier := generate G {x}\<rparr>) {x}"
+        using generate_consistent[OF generate_sincl H.subgroup_axioms] by simp
+    qed
+  qed
+  have ox: "H.ord x = ord x" using H.gen_closed H.subgroup_axioms subgroup_ord_eq by auto
+  have ogt1: "ord x > 1" using ord_pos by (metis assms(1, 2) less_one nat_neq_iff ord_eq_1)
+  from assms H.unity_root_induce_char[unfolded H.ord_gen_is_group_order[symmetric] ox, OF assms(3)]
+  obtain c where c: "character (G\<lparr>carrier := generate G {x}\<rparr>) c"
+                    "c = (\<lambda>a. if a \<in> carrier (G\<lparr>carrier := generate G {x}\<rparr>)
+                              then z powi H.get_exp x a else 0)" by blast
+  have cx: "c x = z" unfolding c(2)
+    using H.powi_get_exp_self[OF assms(3) _ ox ogt1] generate_sincl[of "{x}"] by simp
+  obtain f where f: "character G f" "\<And>y. y \<in> (generate G {x}) \<Longrightarrow> f y = c y"
+    using character_extension_exists[OF H.subgroup_axioms c(1)] by blast
+  show ?thesis by (intro that[OF f(1)], use cx f(2) generate_sincl in blast)
 qed
 
 text \<open>
   In particular, for any \<open>x\<close> that is not the identity element, there exists a character \<open>\<chi>\<close>
   such that $\chi(x)\neq 1$.
 \<close>
-corollary character_neq_1_exists:
+corollary (in finite_comm_group) character_neq_1_exists:
   assumes "x \<in> carrier G" and "x \<noteq> \<one>"
   obtains \<chi> where "character G \<chi>" and "\<chi> x \<noteq> 1"
 proof -
   define z where "z = cis (2 * pi / ord x)"
   have z_pow_h: "z ^ ord x = 1"
     by (auto simp: z_def DeMoivre)
 
   from assms have "ord x \<ge> 1" by (intro ord_ge_1) auto
   moreover have "ord x \<noteq> 1"
     using pow_ord_eq_1[of x] assms fin by (intro notI) simp_all
   ultimately have "ord x > 1" by linarith
 
   have [simp]: "z \<noteq> 1"
   proof
     assume "z = 1"
     have "bij_betw (\<lambda>k. cis (2 * pi * real k / real (ord x))) {..<ord x} {z. z ^ ord x = 1}"
       using \<open>ord x > 1\<close> by (intro bij_betw_roots_unity) auto
     hence inj: "inj_on (\<lambda>k. cis (2 * pi * real k / real (ord x))) {..<ord x}"
       by (auto simp: bij_betw_def)
     have "0 = (1 :: nat)"
       using \<open>z = 1\<close> and \<open>ord x > 1\<close> by (intro inj_onD[OF inj]) (auto simp: z_def)
     thus False by simp
   qed
 
   obtain \<chi> where "character G \<chi>" and "\<chi> x = z"
     using character_with_value_exists[OF assms z_pow_h] .
   thus ?thesis using that[of \<chi>] by simp
-qed 
-
-end
-
+qed
 
 subsection \<open>The first orthogonality relation\<close>
 
 text \<open>
   The entries of any non-principal character sum to 0.
 \<close>
 theorem (in character) sum_character:
   "(\<Sum>x\<in>carrier G. \<chi> x) = (if \<chi> = principal_char G then of_nat (order G) else 0)"
 proof (cases "\<chi> = principal_char G")
   case True
   hence "(\<Sum>x\<in>carrier G. \<chi> x) = (\<Sum>x\<in>carrier G. 1)"
     by (intro sum.cong) (auto simp: principal_char_def)
   also have "\<dots> = order G" by (simp add: order_def)
   finally show ?thesis using True by simp
 next
   case False
   define S where "S = (\<Sum>x\<in>carrier G. \<chi> x)"
   from False obtain y where y: "y \<in> carrier G" "\<chi> y \<noteq> 1"
     by (auto simp: principal_char_def fun_eq_iff char_eq_0_iff split: if_splits)
   from y have "S = (\<Sum>x\<in>carrier G. \<chi> (y \<otimes> x))" unfolding S_def
     by (intro sum.reindex_bij_betw [symmetric] bij_betw_mult_left)
   also have "\<dots> = (\<Sum>x\<in>carrier G. \<chi> y * \<chi> x)"
     by (intro sum.cong refl char_mult y)
   also have "\<dots> = \<chi> y * S" by (simp add: S_def sum_distrib_left)
   finally have "(\<chi> y - 1) * S = 0" by (simp add: algebra_simps)
   with y have "S = 0" by simp
   with False show ?thesis by (simp add: S_def)
 qed
 
 corollary (in finite_comm_group) character_orthogonality1:
   assumes "character G \<chi>" and "character G \<chi>'"
   shows   "(\<Sum>x\<in>carrier G. \<chi> x * cnj (\<chi>' x)) = (if \<chi> = \<chi>' then of_nat (order G) else 0)"
 proof -
   define C where [simp]: "C = Characters G"
   interpret C: finite_comm_group C unfolding C_def
     by (rule finite_comm_group_Characters)
   let ?\<chi> = "\<lambda>x. \<chi> x * inv_character \<chi>' x"
   interpret character G "\<lambda>x. \<chi> x * inv_character \<chi>' x"
     by (intro character_mult character.inv_character assms)
   have "(\<Sum>x\<in>carrier G. \<chi> x * cnj (\<chi>' x)) = (\<Sum>x\<in>carrier G. ?\<chi> x)"
     by (intro sum.cong) (auto simp: inv_character_def)
   also have "\<dots> = (if ?\<chi> = principal_char G then of_nat (order G) else 0)"
     by (rule sum_character)
   also have "?\<chi> = principal_char G \<longleftrightarrow> \<chi> \<otimes>\<^bsub>C\<^esub> inv\<^bsub>C\<^esub> \<chi>' = \<one>\<^bsub>C\<^esub>"
     using assms by (simp add: Characters_simps characters_def)
   also have "\<dots> \<longleftrightarrow> \<chi> = \<chi>'"
   proof
     assume "\<chi> \<otimes>\<^bsub>C\<^esub> inv\<^bsub>C\<^esub> \<chi>' = \<one>\<^bsub>C\<^esub>"
     from C.inv_equality [OF this] and assms show "\<chi> = \<chi>'"
       by (auto simp: characters_def Characters_simps)
   next
     assume *: "\<chi> = \<chi>'"
     from assms show "\<chi> \<otimes>\<^bsub>C\<^esub> inv\<^bsub>C\<^esub> \<chi>' = \<one>\<^bsub>C\<^esub>" 
       by (subst *, intro C.r_inv) (auto simp: carrier_Characters characters_def)
   qed
   finally show ?thesis .
 qed
 
 
 subsection \<open>The isomorphism between a group and its double dual\<close>
 
 text \<open>
   Lastly, we show that the double dual of a finite abelian group is naturally isomorphic
   to the original group via the obvious isomorphism $x\mapsto (\chi\mapsto \chi(x))$.
   It is easy to see that this is a homomorphism and that it is injective. The fact 
   $|\widehat{\widehat{G}}| = |\widehat{G}| = |G|$ then shows that it is also surjective.
 \<close>
 context finite_comm_group
 begin
 
 definition double_dual_iso :: "'a \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> complex" where
   "double_dual_iso x = (\<lambda>\<chi>. if character G \<chi> then \<chi> x else 0)"
 
 lemma double_dual_iso_apply [simp]: "character G \<chi> \<Longrightarrow> double_dual_iso x \<chi> = \<chi> x"
   by (simp add: double_dual_iso_def)
 
 lemma character_double_dual_iso [intro]:
   assumes x: "x \<in> carrier G"
   shows   "character (Characters G) (double_dual_iso x)"
 proof -
   interpret G': finite_comm_group "Characters G"
     by (rule finite_comm_group_Characters)
   show "character (Characters G) (double_dual_iso x)"
     using x by unfold_locales (auto simp: double_dual_iso_def characters_def Characters_def
                                               principal_char_def character.char_eq_0)
 qed
 
 lemma double_dual_iso_mult [simp]:
   assumes "x \<in> carrier G" "y \<in> carrier G"
   shows   "double_dual_iso (x \<otimes> y) =
              double_dual_iso x \<otimes>\<^bsub>Characters (Characters G)\<^esub> double_dual_iso y"
   using assms by (auto simp: double_dual_iso_def Characters_def fun_eq_iff character.char_mult)
 
 lemma double_dual_iso_one [simp]:
   "double_dual_iso \<one> = principal_char (Characters G)"
   by (auto simp: fun_eq_iff double_dual_iso_def principal_char_def
                  carrier_Characters characters_def character.char_one)
 
 lemma inj_double_dual_iso: "inj_on double_dual_iso (carrier G)"
 proof -
   interpret G': finite_comm_group "Characters G"
     by (rule finite_comm_group_Characters)
   interpret G'': finite_comm_group "Characters (Characters G)"
     by (rule G'.finite_comm_group_Characters)
   have hom: "double_dual_iso \<in> hom G (Characters (Characters G))"
     by (rule homI) (auto simp: carrier_Characters characters_def)
   have inj_aux: "x = \<one>"
     if x: "x \<in> carrier G" "double_dual_iso x = \<one>\<^bsub>Characters (Characters G)\<^esub>" for x
   proof (rule ccontr)
     assume "x \<noteq> \<one>"
     obtain \<chi> where \<chi>: "character G \<chi>" "\<chi> x \<noteq> 1"
       using character_neq_1_exists[OF x(1) \<open>x \<noteq> \<one>\<close>] .
     from x have "\<forall>\<chi>. (if \<chi> \<in> characters G then \<chi> x else 0) = (if \<chi> \<in> characters G then 1 else 0)"
       by (auto simp: double_dual_iso_def Characters_def fun_eq_iff
                      principal_char_def characters_def)
     hence eq1: "\<forall>\<chi>\<in>characters G. \<chi> x = 1" by metis
     with \<chi> show False unfolding characters_def by auto
   qed
   thus ?thesis
     using inj_aux hom is_group G''.is_group by (subst inj_on_one_iff') auto
 qed
 
 lemma double_dual_iso_eq_iff [simp]:
   "x \<in> carrier G \<Longrightarrow> y \<in> carrier G \<Longrightarrow> double_dual_iso x = double_dual_iso y \<longleftrightarrow> x = y"
   by (auto dest: inj_onD[OF inj_double_dual_iso])
 
 theorem double_dual_iso: "double_dual_iso \<in> iso G (Characters (Characters G))"
 proof (rule isoI)
   interpret G': finite_comm_group "Characters G"
     by (rule finite_comm_group_Characters)
   interpret G'': finite_comm_group "Characters (Characters G)"
     by (rule G'.finite_comm_group_Characters)
 
   show hom: "double_dual_iso \<in> hom G (Characters (Characters G))"
     by (rule homI) (auto simp: carrier_Characters characters_def)
 
   show "bij_betw double_dual_iso (carrier G) (carrier (Characters (Characters G)))"
     unfolding bij_betw_def
   proof
     show "inj_on double_dual_iso (carrier G)" by (fact inj_double_dual_iso)
   next
     show "double_dual_iso ` carrier G = carrier (Characters (Characters G))"
     proof (rule card_subset_eq)
       show "finite (carrier (Characters (Characters G)))"
         by (fact G''.fin)
     next
       have "card (carrier (Characters (Characters G))) = card (carrier G)"
         by (simp add: carrier_Characters G'.card_characters card_characters order_def)
       also have "\<dots> = card (double_dual_iso ` carrier G)"
         by (intro card_image [symmetric] inj_double_dual_iso)
       finally show "card (double_dual_iso ` carrier G) =
                       card (carrier (Characters (Characters G)))" ..
     next
       show "double_dual_iso ` carrier G \<subseteq> carrier (Characters (Characters G))"
         using hom by (auto simp: hom_def)
     qed
   qed
 qed
 
 lemma double_dual_is_iso: "Characters (Characters G) \<cong> G"
   by (rule iso_sym) (use double_dual_iso in \<open>auto simp: is_iso_def\<close>)
 
 text \<open>
   The second orthogonality relation follows from the first one via Pontryagin duality:
 \<close>
 theorem sum_characters:
   assumes x: "x \<in> carrier G"
   shows   "(\<Sum>\<chi>\<in>characters G. \<chi> x) = (if x = \<one> then of_nat (order G) else 0)"
 proof -
   interpret G': finite_comm_group "Characters G"
     by (rule finite_comm_group_Characters)
   interpret x: character "Characters G" "double_dual_iso x"
     using x by auto
   from x.sum_character show ?thesis using double_dual_iso_eq_iff[of x \<one>] x
-    by (auto simp: characters_def carrier_Characters simp del: double_dual_iso_eq_iff)
+    by (auto simp: characters_def carrier_Characters order_Characters simp del: double_dual_iso_eq_iff)
 qed
 
 corollary character_orthogonality2:
   assumes "x \<in> carrier G" "y \<in> carrier G"
   shows   "(\<Sum>\<chi>\<in>characters G. \<chi> x * cnj (\<chi> y)) = (if x = y then of_nat (order G) else 0)"
 proof -
   from assms have "(\<Sum>\<chi>\<in>characters G. \<chi> x * cnj (\<chi> y)) = (\<Sum>\<chi>\<in>characters G. \<chi> (x \<otimes> inv y))"
     by (intro sum.cong) (simp_all add: character.char_inv character.char_mult characters_def)
   also from assms have "\<dots> = (if x \<otimes> inv y = \<one> then of_nat (order G) else 0)"
     by (intro sum_characters) auto
   also from assms have "x \<otimes> inv y = \<one> \<longleftrightarrow> x = y"
     using inv_equality[of x "inv y"] by auto
   finally show ?thesis .
 qed
 
 end
 
+no_notation integer_mod_group ("Z")
 end
diff --git a/thys/Dirichlet_L/ROOT b/thys/Dirichlet_L/ROOT
--- a/thys/Dirichlet_L/ROOT
+++ b/thys/Dirichlet_L/ROOT
@@ -1,25 +1,26 @@
 chapter AFP
 
 session Dirichlet_L (AFP) = "Zeta_Function" +
   options [timeout = 1200]
   sessions
     "HOL-Analysis"
     "HOL-Algebra"
     "HOL-Library"
     "Landau_Symbols"
     "Dirichlet_Series"
     "Zeta_Function"
     "Bertrands_Postulate"
+    "Finitely_Generated_Abelian_Groups"
   theories [document = false]
     "HOL-Library.Landau_Symbols"
     "Zeta_Function.Zeta_Function"
     "HOL-Number_Theory.Residues"
     "Dirichlet_Series.Multiplicative_Function"
     "HOL-Algebra.Multiplicative_Group"
     "Bertrands_Postulate.Bertrand"
   theories
     Dirichlet_Theorem
   document_files
     "root.tex"
     "root.bib"
 
diff --git a/thys/Finitely_Generated_Abelian_Groups/Finitely_Generated_Abelian_Groups.thy b/thys/Finitely_Generated_Abelian_Groups/Finitely_Generated_Abelian_Groups.thy
--- a/thys/Finitely_Generated_Abelian_Groups/Finitely_Generated_Abelian_Groups.thy
+++ b/thys/Finitely_Generated_Abelian_Groups/Finitely_Generated_Abelian_Groups.thy
@@ -1,982 +1,982 @@
 (*
     File:     Finitely_Generated_Abelian_Groups.thy
     Author:   Joseph Thommes, TU München
 *)
 section \<open>Fundamental Theorem of Finitely Generated Abelian Groups\<close>
 
 theory Finitely_Generated_Abelian_Groups
   imports DirProds Group_Relations
 begin
 
 notation integer_mod_group ("Z")
 
 locale fin_gen_comm_group = comm_group +
   fixes gen :: "'a set"
   assumes gens_closed: "gen \<subseteq> carrier G"
   and     fin_gen: "finite gen"
   and     generators: "carrier G = generate G gen"
 
 text \<open>Every finite abelian group is also finitely generated.\<close>
 
 sublocale finite_comm_group \<subseteq> fin_gen_comm_group G "carrier G"
   using generate_incl generate_sincl by (unfold_locales, auto)
 
 text \<open>This lemma contains the proof of Kemper from his lecture notes on algebra~\cite{kemper}.
 However, the proof is not done in the context of a finitely generated group but for a finitely
 generated subgroup in a commutative group.\<close>
 
 lemma (in comm_group) ex_idirgen:
   fixes A :: "'a set"
   assumes "finite A" "A \<subseteq> carrier G"
   shows "\<exists>gs. set gs \<subseteq> generate G A \<and> distinct gs \<and> is_idirprod (generate G A) (\<lambda>g. generate G {g}) (set gs)
             \<and> successively (dvd) (map ord gs) \<and> card (set gs) \<le> card A"
   (is "?t A")
   using assms
 proof (induction "card A" arbitrary: A rule: nat_less_induct)
   case i: 1
   show ?case
   proof (cases "relations A = {restrict (\<lambda>_. 0::int) A}") (* only trivial relation *)
     case True
     have fi: "finite A" by fact
     then obtain gs where gs: "set gs = A" "distinct gs" by (meson finite_distinct_list)
     have o: "ord g = 0" if "g \<in> set gs" for g
       by (intro relations_zero_imp_ord_zero[OF that], use i(3) that True gs in auto)
     have m: "map ord gs = replicate (length gs) 0" using o
       by (induction gs; auto)
     show ?thesis
-    proof(intro exI conjI subsetI)
+    proof(rule, safe)
       show "\<And>x. x \<in> set gs \<Longrightarrow> x \<in> generate G A" using gs generate.incl[of _ A G] by blast
       show "distinct gs" by fact
       show "is_idirprod (generate G A) (\<lambda>g. generate G {g}) (set gs)"
       proof(unfold is_idirprod_def, intro conjI, rule)
         show "generate G {g} \<lhd> G" if "g \<in> set gs" for g
           by (intro subgroup_imp_normal, use that generate_is_subgroup i(3) gs in auto)
         show "generate G A = IDirProds G (\<lambda>g. generate G {g}) (set gs)" unfolding IDirProds_def
           by (subst gs(1), use generate_idem_Un i(3) in blast)
         show "compl_fam (\<lambda>g. generate G {g}) (set gs)" using compl_fam_iff_relations_triv[OF i(2, 3)] o gs(1) True
           by blast 
       qed
       show "successively (dvd) (map ord gs)" using m
       proof (induction gs)
         case c: (Cons a gs)
         thus ?case by(cases gs; simp)
       qed simp
       show "card (set gs) \<le> card A" using gs by blast
     qed
   next
     case ntrel: False
     then have Ane: "A \<noteq> {}"
       using i(2) triv_rel[of A] unfolding relations_def extensional_def by fastforce
     from ntrel obtain a where a: "a \<in> A" "\<exists>r \<in>relations A. r a \<noteq> 0" using i(2) triv_rel[of A]
       unfolding relations_def extensional_def by fastforce
     hence ac: "a \<in> carrier G" using i(3) by blast
     have iH: "\<And>B.\<lbrakk>card B < card A; finite B; B \<subseteq> carrier G\<rbrakk> \<Longrightarrow> ?t B"
       using i(1) by blast
     have iH2: "\<And>B. \<lbrakk>?t B; generate G A = generate G B; card B < card A\<rbrakk> \<Longrightarrow> ?t A"
       by fastforce
     show ?thesis
     proof(cases "inv a \<in> (A - {a})")
       case True
       have "generate G A = generate G (A - {a})"
       proof(intro generate_subset_eqI[OF i(3)])
         show "A - (A - {a}) \<subseteq> generate G (A - {a})"
         proof -
           have "A - (A - {a}) = {a}" using a True by auto
           also have "\<dots> \<subseteq> generate G {inv a}" using generate.inv[of "inv a" "{inv a}" G] ac by simp
           also have "\<dots> \<subseteq> generate G (A - {a})" by (intro mono_generate, use True in simp)
           finally show ?thesis .
         qed
       qed simp
       moreover have "?t (A - {a})"
         by (intro iH[of "A - {a}"], use i(2, 3) a(1) in auto, meson Ane card_gt_0_iff diff_Suc_less)
       ultimately show ?thesis using card.remove[OF i(2) a(1)] by fastforce
     next
       case inv: False
       define n where n: "n = card A"
       define all_gens where
         "all_gens = {gs\<in>Pow (generate G A). finite gs \<and> card gs \<le> n \<and> generate G gs = generate G A}"
 
       define exps where "exps = (\<Union>gs'\<in>all_gens. \<Union>rel\<in>relations gs'. nat ` {e\<in>rel`gs'. e > 0})"
       define min_exp where "min_exp = Inf exps"
 
       have "exps \<noteq> {}"
       proof -
         let ?B = "A - {a} \<union> {inv a}"
         have "A \<in> all_gens" unfolding all_gens_def using generate.incl n i(2) by fast
         moreover have "?B \<in> all_gens"
         proof -
           have "card (A - {a}) = n - 1" using a n by (meson card_Diff_singleton_if i(2))
           hence "card ?B = n" using inv i(2, 3) n a(1)
             by (metis Un_empty_right Un_insert_right card.remove card_insert_disjoint finite_Diff) 
           moreover have "generate G A = generate G ?B"
           proof(intro generate_one_switched_eqI[OF i(3) a(1), of _ "inv a"])
             show "inv a \<in> generate G A" using generate.inv[OF a(1), of G] .
             show "a \<in> generate G ?B"
             proof -
               have "a \<in> generate G {inv a}" using generate.inv[of "inv a" "{inv a}" G] ac by simp
               also have "\<dots> \<subseteq> generate G ?B" by (intro mono_generate, blast)
               finally show ?thesis .
             qed
           qed simp
           moreover hence "?B \<subseteq> generate G A" using generate_sincl by simp
           ultimately show ?thesis unfolding all_gens_def using i(2) by blast
         qed
         moreover have "(\<exists>r \<in> relations A. r a > 0) \<or> (\<exists>r \<in> relations ?B. r (inv a) > 0)"
         proof(cases "\<exists>r \<in> relations A. r a > 0")
           case True
           then show ?thesis by blast
         next
           case False
           with a obtain r where r: "r \<in> relations A" "r a < 0" by force
           have rc: "(\<lambda>x. x [^] r x) \<in> A \<rightarrow> carrier G" using i(3) int_pow_closed by fast
           let ?r = "restrict (r(inv a := - r a)) ?B"
           have "?r \<in> relations ?B"
           proof
             have "finprod G (\<lambda>x. x [^] ?r x) ?B = finprod G (\<lambda>x. x [^] r x) A"
             proof -
               have "finprod G (\<lambda>x. x [^] ?r x) ?B
                   = finprod G (\<lambda>x. x [^] ?r x) (insert (inv a) (A - {a}))" by simp
               also have "\<dots> = (inv a) [^] ?r (inv a) \<otimes> finprod G (\<lambda>x. x [^] ?r x) (A - {a})"
               proof(intro finprod_insert[OF _ inv])
                 show "finite (A - {a})" using i(2) by fast
                 show "inv a [^] ?r (inv a) \<in> carrier G"
                   using int_pow_closed[OF inv_closed[OF ac]] by fast
                 show "(\<lambda>x. x [^] ?r x) \<in> A - {a} \<rightarrow> carrier G" using int_pow_closed i(3) by fast
               qed
               also have "\<dots> = a [^] r a \<otimes> finprod G (\<lambda>x. x [^] r x) (A - {a})"
               proof -
                 have "(inv a) [^] ?r (inv a) = a [^] r a"
                   by (simp add: int_pow_inv int_pow_neg ac)
                 moreover have "finprod G (\<lambda>x. x [^] r x) (A - {a})
                              = finprod G (\<lambda>x. x [^] ?r x) (A - {a})"
                 proof(intro finprod_cong)
                   show "((\<lambda>x. x [^] r x) \<in> A - {a} \<rightarrow> carrier G) = True" using rc by blast
                   have "i [^] r i = i [^] ?r i" if "i \<in> A - {a}" for i using that inv by auto
                   thus "\<And>i. i \<in> A - {a} =simp=> i [^] r i = i [^] restrict (r(inv a := - r a)) (A - {a} \<union> {inv a}) i"
                     by algebra
                 qed simp
                 ultimately show ?thesis by argo
               qed
               also have "\<dots> = finprod G (\<lambda>x. x [^] r x) A"
                 by (intro finprod_minus[symmetric, OF a(1) rc i(2)])
               finally show ?thesis .
             qed
             also have "\<dots> = \<one>" using r unfolding relations_def by fast
             finally show "finprod G (\<lambda>x. x [^] ?r x) ?B = \<one>" .
           qed simp
           then show ?thesis using r by fastforce
         qed
         ultimately show ?thesis unfolding exps_def using a by blast
       qed
       hence me: "min_exp \<in> exps"
         unfolding min_exp_def using Inf_nat_def1 by force
       from cInf_lower min_exp_def have le: "\<And>x. x \<in> exps \<Longrightarrow> min_exp \<le> x" by blast
       from me obtain gs rel g
         where gr: "gs \<in> all_gens" "rel \<in> relations gs" "g \<in> gs" "rel g = min_exp" "min_exp > 0"
         unfolding exps_def by auto
       from gr(1) have cgs: "card gs \<le> card A" unfolding all_gens_def n by blast
       with gr(3) have cgsg: "card (gs - {g}) < card A"
         by (metis Ane card.infinite card_Diff1_less card_gt_0_iff finite.emptyI
                   finite.insertI finite_Diff2 i.prems(1) le_neq_implies_less less_trans)
       from gr(1) have fgs: "finite gs" and gsg: "generate G gs = generate G A"
         unfolding all_gens_def n using i(2) card.infinite Ane by force+
       from gsg have gsc: "gs \<subseteq> carrier G" unfolding all_gens_def
         using generate_incl[OF i(3)] generate_sincl[of gs] by simp
       hence gc: "g \<in> carrier G" using gr(3) by blast
       have ihgsg: "?t (gs - {g})"
         by (intro iH, use cgs fgs gsc gr(3) cgsg in auto)
       then obtain hs where
         hs: "set hs \<subseteq> generate G (gs - {g})" "distinct hs"
             "is_idirprod (generate G (gs - {g})) (\<lambda>g. generate G {g}) (set hs)"
             "successively (dvd) (map ord hs)" "card (set hs) \<le> card (gs - {g})" by blast
       hence hsc: "set hs \<subseteq> carrier G"
         using generate_sincl[of "set hs"] generate_incl[of "gs - {g}"] gsc by blast
       from hs(3) have ghs: "generate G (gs - {g}) = generate G (set hs)"
         unfolding is_idirprod_def IDirProds_def using generate_idem_Un[OF hsc] by argo
       have dvot: "?t A \<or> (\<forall>e\<in>rel`gs. rel g dvd e)"
       proof(intro disjCI)
         assume na: "\<not> (\<forall>e\<in>rel ` gs. rel g dvd e)"
         have "\<And>x. \<lbrakk>x \<in> gs; \<not>rel g dvd rel x\<rbrakk> \<Longrightarrow> ?t A"
         proof -
           fix x
           assume x: "x \<in> gs" "\<not> rel g dvd rel x"
           hence xng: "x \<noteq> g" by auto
           from x have xc: "x \<in> carrier G" using gsc by blast
           have rg: "rel g > 0" using gr by simp
           define r::int where r: "r = rel x mod rel g"
           define q::int where q: "q = rel x div rel g"
           from r rg x have "r > 0"
             using mod_int_pos_iff[of "rel x" "rel g"] mod_eq_0_iff_dvd by force
           moreover have "r < rel g" using r rg Euclidean_Division.pos_mod_bound by blast
           moreover have "rel x = q * rel g + r" using r q by presburger
           ultimately have rq: "rel x = q * (rel g) + r" "0 < r" "r < rel g" by auto
           define t where t: "t = g \<otimes> x [^] q"
           hence tc: "t \<in> carrier G" using gsc gr(3) x by fast
           define s where s: "s = gs - {g} \<union> {t}"
           hence fs: "finite s" using fgs by blast
           have sc: "s \<subseteq> carrier G" using s tc gsc by blast
           have g: "generate G gs = generate G s"
           proof(unfold s, intro generate_one_switched_eqI[OF gsc gr(3), of _ t])
             show "t \<in> generate G gs"
             proof(unfold t, intro generate.eng)
               show "g \<in> generate G gs" using gr(3) generate.incl by fast
               show "x [^] q \<in> generate G gs"
                 using x generate_pow[OF xc] generate_sincl[of "{x}"] mono_generate[of "{x}" gs]
                 by fast
             qed
             show "g \<in> generate G (gs - {g} \<union> {t})"
             proof -
               have gti: "g = t \<otimes> inv (x [^] q)"
                 using inv_solve_right[OF gc tc int_pow_closed[OF xc, of q]] t by blast
               moreover have "t \<in> generate G (gs - {g} \<union> {t})" by (intro generate.incl[of t], simp)
               moreover have "inv (x [^] q) \<in> generate G (gs - {g})"
               proof -
                 have "x [^] q \<in> generate G {x}" using generate_pow[OF xc] by blast
                 from generate_m_inv_closed[OF _ this] xc
                 have "inv (x [^] q) \<in> generate G {x}" by blast
                 moreover have "generate G {x} \<subseteq> generate G (gs - {g})"
                   by (intro mono_generate, use x a in force)
                 finally show ?thesis .
               qed
               ultimately show ?thesis
                 using generate.eng mono_generate[of "gs - {g}" "gs - {g} \<union> {t}"] by fast
             qed
           qed simp
           show "\<lbrakk>x \<in> gs; \<not> rel g dvd rel x\<rbrakk> \<Longrightarrow> ?t A"
           proof (cases "t \<in> gs - {g}")
             case xt: True
             from xt have gts: "s = gs - {g}" using x s by auto
             moreover have "card (gs - {g}) < card gs" using fgs gr(3) by (meson card_Diff1_less)
             ultimately have "card (set hs) < card A" using hs(5) cgs by simp
             moreover have "set hs \<subseteq> generate G (set hs)" using generate_sincl by simp
             moreover have "distinct hs" by fact
             moreover have "is_idirprod (generate G (set hs)) (\<lambda>g. generate G {g}) (set hs)"
               using hs ghs unfolding is_idirprod_def by blast
             moreover have "generate G A = generate G (set hs)" using g gts ghs gsg by argo
             moreover have "successively (dvd) (map ord hs)" by fact
             ultimately show "?t A" using iH2 by blast
           next
             case tngsg: False
             hence xnt: "x \<noteq> t" using x xng by blast
             have "rel g dvd rel x"
             proof (rule ccontr)
               have "nat r \<in> exps" unfolding exps_def
               proof
                 show "s \<in> all_gens" unfolding all_gens_def
                   using gsg g fgs generate_sincl[of s] switch_elem_card_le[OF gr(3), of t] cgs n s
                   by auto
                 have xs: "x \<in> s" using s xng x(1) by blast
                 have ts: "t \<in> s" using s by fast
                 show "nat r \<in> (\<Union>rel\<in>relations s. nat ` {e \<in> rel ` s. 0 < e})"
                 proof
                   let ?r = "restrict (rel(x := r, t := rel g)) s"
                   show "?r \<in> relations s"
                   proof
                     have "finprod G (\<lambda>x. x [^] ?r x) s = finprod G (\<lambda>x. x [^] rel x) gs"
                     proof -
                       have "finprod G (\<lambda>x. x [^] ?r x) s = x [^] r \<otimes> (t [^] rel g \<otimes> finprod G (\<lambda>x. x [^] rel x) (gs - {g} - {x}))"
                       proof -
                         have "finprod G (\<lambda>x. x [^] ?r x) s = x [^] ?r x \<otimes> finprod G (\<lambda>x. x [^] ?r x) (s - {x})"
                           by (intro finprod_minus[OF xs _ fs], use sc in auto) 
                         moreover have "finprod G (\<lambda>x. x [^] ?r x) (s - {x}) = t [^] ?r t \<otimes> finprod G (\<lambda>x. x [^] ?r x) (s - {x} - {t})"
                           by (intro finprod_minus, use ts xnt fs sc in auto)
                         moreover have "finprod G (\<lambda>x. x [^] ?r x) (s - {x} - {t}) = finprod G (\<lambda>x. x [^] rel x) (s - {x} - {t})"
                           unfolding s by (intro finprod_cong',  use gsc in auto)
                         moreover have "s - {x} - {t} = gs - {g} - {x}" unfolding s using tngsg by blast
                         moreover hence "finprod G (\<lambda>x. x [^] rel x) (s - {x} - {t}) = finprod G (\<lambda>x. x [^] rel x) (gs - {g} - {x})" by simp
                         moreover have "x [^] ?r x = x [^] r" using xs xnt by auto
                         moreover have "t [^] ?r t = t [^] rel g" using ts by simp
                         ultimately show ?thesis by argo
                       qed
                       also have "\<dots> = x [^] r \<otimes> t [^] rel g \<otimes> finprod G (\<lambda>x. x [^] rel x) (gs - {g} - {x})"
                         by (intro m_assoc[symmetric], use xc tc in simp_all, intro finprod_closed, use gsc in fast)
                       also have "\<dots> = g [^] rel g \<otimes> x [^] rel x \<otimes> finprod G (\<lambda>x. x [^] rel x) (gs - {g} - {x})"
                       proof -
                         have "x [^] r \<otimes> t [^] rel g = g [^] rel g \<otimes> x [^] rel x"
                         proof -
                           have "x [^] r \<otimes> t [^] rel g = x [^] r \<otimes> (g \<otimes> x [^] q) [^] rel g" using t by blast
                           also have "\<dots> = x [^] r \<otimes> x [^] (q * rel g) \<otimes> g [^] rel g"
                           proof -
                             have "(g \<otimes> x [^] q) [^] rel g = g [^] rel g \<otimes> (x [^] q) [^] rel g"
                               using gc xc int_pow_distrib by auto
                             moreover have "(x [^] q) [^] rel g = x [^] (q * rel g)" using xc int_pow_pow by auto
                             moreover have "g [^] rel g \<otimes> x [^] (q * rel g) = x [^] (q * rel g) \<otimes> g [^] rel g"
                               using m_comm[OF int_pow_closed[OF xc] int_pow_closed[OF gc]] by simp
                             ultimately have "(g \<otimes> x [^] q) [^] rel g = x [^] (q * rel g) \<otimes> g [^] rel g" by argo
                             thus ?thesis by (simp add: gc m_assoc xc)
                           qed
                           also have "\<dots> = x [^] rel x \<otimes> g [^] rel g"
                           proof -
                             have "x [^] r \<otimes> x [^] (q * rel g) = x [^] (q * rel g + r)"
                               by (simp add: add.commute int_pow_mult xc)
                             also have "\<dots> = x [^] rel x" using rq by argo
                             finally show ?thesis by argo
                           qed
                           finally show ?thesis by (simp add: gc m_comm xc)
                         qed
                         thus ?thesis by simp
                       qed
                       also have "\<dots> = g [^] rel g \<otimes> (x [^] rel x \<otimes> finprod G (\<lambda>x. x [^] rel x) (gs - {g} - {x}))"
                         by (intro m_assoc, use xc gc in simp_all, intro finprod_closed, use gsc in fast)
                       also have "\<dots> = g [^] rel g \<otimes> finprod G (\<lambda>x. x [^] rel x) (gs - {g})"
                       proof -
                         have "finprod G (\<lambda>x. x [^] rel x) (gs - {g}) = x [^] rel x \<otimes> finprod G (\<lambda>x. x [^] rel x) (gs - {g} - {x})"
                           by (intro finprod_minus, use xng x(1) fgs gsc in auto)
                         thus ?thesis by argo
                       qed
                       also have "\<dots> = finprod G (\<lambda>x. x [^] rel x) gs" by (intro finprod_minus[symmetric, OF gr(3) _ fgs], use gsc in auto)
                       finally show ?thesis .
                     qed                        
                     thus "finprod G (\<lambda>x. x [^] ?r x) s = \<one>" using gr(2) unfolding relations_def by simp
                   qed auto
                   show "nat r \<in> nat ` {e \<in> ?r ` s. 0 < e}" using xs xnt rq(2) by fastforce
                 qed
               qed
               from le[OF this] rq(3) gr(4, 5) show False by linarith
             qed
             thus "\<lbrakk>x \<in> gs; \<not> rel g dvd rel x\<rbrakk> \<Longrightarrow> ?t A" by blast
           qed
         qed
         thus "?t A" using na by blast
       qed
       show "?t A"
       proof (cases "\<forall>e\<in>rel`gs. rel g dvd e")
         case dv: True
         define tau where "tau = finprod G (\<lambda>x. x [^] ((rel x) div rel g)) gs"
         have tc: "tau \<in> carrier G"
           by (subst tau_def, intro finprod_closed[of "(\<lambda>x. x [^] ((rel x) div rel g))" gs], use gsc in fast) 
         have gts: "generate G gs = generate G (gs - {g} \<union> {tau})"
         proof(intro generate_one_switched_eqI[OF gsc gr(3), of _ tau])
           show "tau \<in> generate G gs" by (subst generate_eq_finprod_Pi_int_image[OF fgs gsc], unfold tau_def, fast)
           show "g \<in> generate G (gs - {g} \<union> {tau})"
           proof -
             have "tau = g \<otimes> finprod G (\<lambda>x. x [^] ((rel x) div rel g)) (gs - {g})"
             proof -
               have "finprod G (\<lambda>x. x [^] ((rel x) div rel g)) gs = g [^] (rel g div rel g) \<otimes> finprod G (\<lambda>x. x [^] ((rel x) div rel g)) (gs - {g})"
                 by (intro finprod_minus[OF gr(3) _ fgs], use gsc in fast)
               moreover have "g [^] (rel g div rel g) = g" using gr gsc by auto
               ultimately show ?thesis unfolding tau_def by argo
             qed
             hence gti: "g = tau \<otimes> inv finprod G (\<lambda>x. x [^] ((rel x) div rel g)) (gs - {g})"
               using inv_solve_right[OF gc tc finprod_closed[of "(\<lambda>x. x [^] ((rel x) div rel g))" "gs - {g}"]] gsc
               by fast
             have "tau \<in> generate G (gs - {g} \<union> {tau})" by (intro generate.incl[of tau], simp)
             moreover have "inv finprod G (\<lambda>x. x [^] ((rel x) div rel g)) (gs - {g}) \<in> generate G (gs - {g})"
             proof -
               have "finprod G (\<lambda>x. x [^] ((rel x) div rel g)) (gs - {g}) \<in> generate G (gs - {g})"
                 using generate_eq_finprod_Pi_int_image[of "gs - {g}"] fgs gsc by fast
               from  generate_m_inv_closed[OF _ this] gsc show ?thesis by blast
             qed
             ultimately show ?thesis by (subst gti, intro generate.eng, use mono_generate[of "gs - {g}"] in auto)
           qed
         qed simp
         with gr(1) have gt: "generate G (gs - {g} \<union> {tau}) = generate G A" unfolding all_gens_def by blast
         have trgo: "tau [^] rel g = \<one>"
         proof -
           have "tau [^] rel g = finprod G (\<lambda>x. x [^] ((rel x) div rel g)) gs [^] rel g" unfolding tau_def by blast
           also have "\<dots> = finprod G ((\<lambda>x. x [^] rel g) \<circ> (\<lambda>x. x [^] ((rel x) div rel g))) gs"
             by (intro finprod_exp, use gsc in auto)
           also have "\<dots> = finprod G (\<lambda>a. a [^] rel a) gs"
           proof(intro finprod_cong')
             show "((\<lambda>x. x [^] rel g) \<circ> (\<lambda>x. x [^] ((rel x) div rel g))) x = x [^] rel x" if "x \<in> gs" for x
             proof -
               have "((\<lambda>x. x [^] rel g) \<circ> (\<lambda>x. x [^] ((rel x) div rel g))) x = x [^] (((rel x) div rel g) * rel g)"
                 using that gsc int_pow_pow by auto
               also have "\<dots> = x [^] rel x" using dv that by auto
               finally show ?thesis .
             qed
           qed (use gsc in auto)
           also have "\<dots> = \<one>" using gr(2) unfolding relations_def by blast
           finally show ?thesis .
         qed
         hence otdrg: "ord tau dvd rel g" using tc int_pow_eq_id by force
         have ot: "ord tau = rel g"
         proof -
           from gr(4, 5) have "rel g > 0" by simp
           with otdrg have "ord tau \<le> rel g" by (meson zdvd_imp_le)
           moreover have "\<not>ord tau < rel g" 
           proof
             assume a: "int (ord tau) < rel g"
             define T where T: "T = gs - {g} \<union> {tau}"
             hence tT: "tau \<in> T" by blast
             let ?r = "restrict ((\<lambda>_.(0::int))(tau := int(ord tau))) T"
             from T have "T \<in> all_gens"
               using gt generate_sincl[of "gs - {g} \<union> {tau}"] switch_elem_card_le[OF gr(3), of tau] fgs cgs n
               unfolding all_gens_def by auto
             moreover have "?r \<in> relations T"
             proof(intro in_relationsI finprod_one_eqI)
               have "tau [^] int (ord tau) = \<one>" using tc pow_ord_eq_1[OF tc] int_pow_int by metis
               thus "x [^] ?r x = \<one>" if "x \<in> T" for x using tT that by(cases "\<not>x = tau", auto)
             qed auto
             moreover have "?r tau = ord tau" using tT by auto
             moreover have "ord tau > 0" using dvd_nat_bounds gr(4) gr(5) int_dvd_int_iff otdrg by presburger
             ultimately have "ord tau \<in> exps" unfolding exps_def using tT by (auto, force)
             with le a gr(4) show False by force
           qed
           ultimately show ?thesis by auto
         qed
         hence otnz: "ord tau \<noteq> 0" using gr me exps_def by linarith
         define l where l: "l = tau#hs"
         hence ls: "set l = set hs \<union> {tau}" by auto
         with hsc tc have slc: "set l \<subseteq> carrier G" by auto
         have gAhst: "generate G A = generate G (set hs \<union> {tau})"
         proof -
           have "generate G A = generate G (gs - {g} \<union> {tau})" using gt by simp
           also have "\<dots> = generate G (set hs \<union> {tau})"
             by (rule generate_subset_change_eqI, use hsc gsc tc ghs in auto)
           finally show ?thesis .
         qed
         have glgA: "generate G (set l) = generate G A" using gAhst ls by simp
         have lgA: "set l \<subseteq> generate G A"
           using ls gt gts hs(1)
                 mono_generate[of "gs - {g}" gs] generate.incl[of tau "gs - {g} \<union> {tau}"]
           by fast
         show ?thesis
         proof (cases "ord tau = 1")
           case True
           hence "tau = \<one>" using ord_eq_1 tc by blast
           hence "generate G A = generate G (gs - {g})"
             using gAhst generate_one_irrel hs(3) ghs by auto
           from iH2[OF ihgsg this cgsg] show ?thesis .
         next
           case otau: False
           consider (nd) "\<not>distinct l" | (ltn) "length l < n \<and> distinct l" | (dn) "length l = n \<and> distinct l"
           proof -
             have "length l \<le> n"
             proof -
               have "length l = length hs + 1" using l by simp
               moreover have "length hs \<le> card (gs - {g})" using hs(2, 5) by (metis distinct_card)
               moreover have "card (gs - {g}) + 1 \<le> n"
                 using n cgsg gr(3) fgs Ane i(2) by (simp add: card_gt_0_iff)
               ultimately show ?thesis by linarith
             qed
             thus "\<lbrakk>\<not> distinct l \<Longrightarrow> thesis; length l < n \<and> distinct l \<Longrightarrow> thesis; length l = n \<and> distinct l \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis"
               by linarith 
           qed
           thus ?thesis
           proof(cases)
             case nd
             with hs(2) l have ths: "set hs = set hs \<union> {tau}" by auto
             hence "set l = set hs" using l by auto
             hence "generate G (gs - {g}) = generate G A" using gAhst ths ghs by argo
             moreover have "card (set hs) \<le> card A"
               by (metis Diff_iff card_mono cgs dual_order.trans fgs hs(5) subsetI)
             ultimately show ?thesis using hs by auto
           next
             case ltn
             then have cl: "card (set l) < card A" using n by (metis distinct_card)
             from iH[OF this] hsc tc ls have "?t (set l)" by blast
             thus ?thesis by (subst (1 2) gAhst, use cl ls in fastforce)
           next
             case dn
             hence ln: "length l = n" and dl: "distinct l" by auto
             have c: "complementary (generate G {tau}) (generate G (gs - {g}))"
             proof -
               have "x = \<one>" if "x \<in> generate G {tau} \<inter> generate G (set hs)" for x
               proof -
                 from that generate_incl[OF hsc] have xc: "x \<in> carrier G" by blast
                 from that have xgt: "x \<in> generate G {tau}" and xgs: "x \<in> generate G (set hs)"
                   by auto
                 from generate_nat_pow[OF otnz tc] xgt have "\<exists>a. a \<ge> 0 \<and> a < ord tau \<and> x = tau [^] a"
                   unfolding atLeastAtMost_def atLeast_def atMost_def
                   by (auto, metis Suc_pred less_Suc_eq_le neq0_conv otnz)
                 then obtain a where a: "0 \<le> a" "a < ord tau" "x = tau [^] a" by blast
                 then have ix: "inv x \<in> generate G (set hs)"
                   using xgs generate_m_inv_closed ghs hsc by blast
                 with generate_eq_finprod_Pi_int_image[OF _ hsc] obtain f where
                   f: "f \<in> Pi (set hs) (\<lambda>_. (UNIV::int set))" "inv x = finprod G (\<lambda>g. g [^] f g) (set hs)"
                   by blast
                 let ?f = "restrict (f(tau := a)) (set l)"
                 have fr: "?f \<in> relations (set l)"
                 proof(intro in_relationsI)
                   from ls dl l have sh: "set hs = set l - {tau}" by auto
                   have "finprod G (\<lambda>a. a [^] ?f a) (set l) = tau [^] ?f tau \<otimes> finprod G (\<lambda>a. a [^] ?f a) (set hs)"
                     by (subst sh, intro finprod_minus, use l slc in auto)
                   moreover have "tau [^] ?f tau = x" using a l int_pow_int by fastforce
                   moreover have "finprod G (\<lambda>a. a [^] ?f a) (set hs) = finprod G (\<lambda>g. g [^] f g) (set hs)"
                     by (intro finprod_cong', use slc dl l in auto)
                   ultimately have "finprod G (\<lambda>a. a [^] ?f a) (set l) = x \<otimes> inv x" using f by argo
                   thus "finprod G (\<lambda>a. a [^] ?f a) (set l) = \<one>" using xc by auto
                 qed blast
                 have "\<not>a > 0"
                 proof
                   assume ag: "0 < a"
                   have "set l \<in> all_gens" unfolding all_gens_def using glgA lgA dn distinct_card
                     by fastforce
                   moreover have "int a = ?f tau" using l by auto
                   moreover have "tau \<in> set l" using l by simp
                   ultimately have "a \<in> exps" using fr ag unfolding exps_def by (auto, force)
                   from le[OF this] a(2) ot gr(4) show False by simp
                 qed
                 hence "a = 0" using a by blast
                 thus "x = \<one>" using tc a by force
               qed
               thus ?thesis unfolding complementary_def using generate.one ghs by blast
             qed
             moreover have idl: "is_idirprod (generate G A) (\<lambda>g. generate G {g}) (set l)" 
             proof -
               have "is_idirprod (generate G (set hs \<union> {tau})) (\<lambda>g. generate G {g}) (set hs \<union> {tau})"
                 by (intro idirprod_generate_ind, use tc hsc hs(3) ghs c in auto)
               thus ?thesis using ls gAhst by auto
             qed
             moreover have "\<not>?t A \<Longrightarrow> successively (dvd) (map ord l)"
             proof (cases hs)
               case Nil
               thus ?thesis using l by simp
             next
               case (Cons a list)
               hence ac: "a \<in> carrier G" using hsc by auto
               assume nA: "\<not>?t A"
               have "ord tau dvd ord a"
               proof (rule ccontr)
                 assume nd: "\<not> ord tau dvd ord a"
                 have "int (ord tau) > 0" using otnz by simp
                 with nd obtain r q::int where rq: "ord a = q * (ord tau) + r" "0 < r" "r < ord tau"
                   using Euclidean_Division.pos_mod_bound div_mult_mod_eq mod_int_pos_iff mod_0_imp_dvd
                   by (metis linorder_not_le of_nat_le_0_iff of_nat_mod)
                 define b where b: "b = tau \<otimes> a [^] q"
                 hence bc: "b \<in> carrier G" using hsc tc Cons by auto
                 have g: "generate G (set (b#hs)) = generate G (set l)"
                 proof -
                   have se: "set (b#hs) = set l - {tau} \<union> {b}" using l Cons dl by auto
                   show ?thesis
                   proof(subst se, intro generate_one_switched_eqI[symmetric, of _ tau _ b])
                     show "b \<in> generate G (set l)"
                     proof -
                       have "tau \<in> generate G (set l)" using l generate.incl[of tau "set l"] by auto
                       moreover have "a [^] q \<in> generate G (set l)" 
                         using mono_generate[of "{a}" "set l"] generate_pow[OF ac] Cons l by auto
                       ultimately show ?thesis using b generate.eng by fast
                     qed
                     show "tau \<in> generate G (set l - {tau} \<union> {b})"
                     proof -
                       have "tau = b \<otimes> inv(a [^] q)" by (simp add: ac b m_assoc tc)
                       moreover have "b \<in> generate G (set l - {tau} \<union> {b})"
                         using generate.incl[of b "set l - {tau} \<union> {b}"] by blast
                       moreover have "inv(a [^] q) \<in> generate G (set l - {tau} \<union> {b})"
                       proof -
                         have "generate G {a} \<subseteq> generate G (set l - {tau} \<union> {b})"
                           using mono_generate[of "{a}" "set l - {tau} \<union> {b}"] dl Cons l by auto
                         moreover have "inv(a [^] q) \<in> generate G {a}"
                           by (subst generate_pow[OF ac], subst int_pow_neg[OF ac, of q, symmetric], blast)
                         ultimately show ?thesis by fast
                       qed
                       ultimately show ?thesis using generate.eng by fast
                     qed
                   qed (use bc tc hsc dl Cons l in auto)
                 qed
                 show False
                 proof (cases "card (set (b#hs)) \<noteq> n")
                   case True
                   hence cln: "card (set (b#hs)) < n"
                     using l Cons ln by (metis card_length list.size(4) nat_less_le)
                   hence seq: "set (b#hs) = set hs"
                   proof -
                     from dn l Cons True have "b \<in> set hs"
                       by (metis distinct.simps(2) distinct_card list.size(4))
                     thus ?thesis by auto
                   qed
                   with cln have clA: "card (set hs) < card A" using n by auto
                   moreover have "set hs \<subseteq> generate G (set hs)" using generate_sincl by simp
                   moreover have "distinct hs" by fact
                   moreover have "is_idirprod (generate G (set hs)) (\<lambda>g. generate G {g}) (set hs)"
                     by (intro is_idirprod_generate, use hs[unfolded is_idirprod_def] hsc in auto)
                   moreover have "generate G A = generate G (set hs)" using glgA g seq by argo
                   moreover have "successively (dvd) (map ord hs)" by fact
                   ultimately show False using iH2 nA by blast
                 next
                   case False
                   hence anb: "a \<noteq> b"
                     by (metis card_distinct distinct_length_2_or_more l list.size(4) ln local.Cons)
                   have "nat r \<in> exps" unfolding exps_def
                   proof(rule)
                     show "set (b#hs) \<in> all_gens" unfolding all_gens_def
                       using gAhst g ls generate_sincl[of "set (b#hs)"] False by simp
                     let ?r = "restrict ((\<lambda>_. 0::int)(b := ord tau, a := r)) (set (b#hs))"
                     have "?r \<in> relations (set (b#hs))"
                     proof(intro in_relationsI)
                       show "finprod G (\<lambda>x. x [^] ?r x) (set (b#hs)) = \<one>"
                       proof -
                         have "finprod G (\<lambda>x. x [^] ?r x) (set (b#hs)) = b [^] ?r b \<otimes> finprod G (\<lambda>x. x[^] ?r x) (set (b#hs) - {b})"
                           by (intro finprod_minus, use hsc Cons bc in auto)
                         moreover have "finprod G (\<lambda>x. x[^] ?r x) (set (b#hs) - {b}) = a [^] ?r a \<otimes> finprod G (\<lambda>x. x[^] ?r x) (set (b#hs) - {b} - {a})"
                           by (intro finprod_minus, use hsc Cons False n anb in auto)
                         moreover have "finprod G (\<lambda>x. x[^] ?r x) (set (b#hs) - {b} - {a}) = \<one>"
                           by (intro finprod_one_eqI, simp)
                         ultimately have "finprod G (\<lambda>x. x [^] ?r x) (set (b#hs)) = b [^] ?r b \<otimes> (a [^] ?r a \<otimes> \<one>)"
                           by argo
                         also have "\<dots> = b [^] ?r b \<otimes> a [^] ?r a" using Cons hsc by simp
                         also have "\<dots> = b [^] int(ord tau) \<otimes> a [^] r" using anb Cons by simp
                         also have "\<dots> = \<one>"
                         proof -
                           have "b [^] int (ord tau) = tau [^] int (ord tau) \<otimes> (a [^] q) [^] int (ord tau)"
                             using b bc hsc int_pow_distrib local.Cons tc by force
                           also have "\<dots> = (a [^] q) [^] int (ord tau)"
                             using trgo hsc local.Cons ot by force
                           finally have "b [^] int (ord tau) \<otimes> a [^] r = (a [^] q) [^] int (ord tau) \<otimes> a [^] r"
                             by argo
                           also have "\<dots> = a [^] (q * int (ord tau) + r)" using Cons hsc
                             by (metis comm_group_axioms comm_group_def group.int_pow_pow
                                       int_pow_mult list.set_intros(1) subsetD)
                           also have "\<dots> = a [^] int (ord a)" using rq by argo
                           finally show ?thesis using Cons hsc int_pow_eq_id by simp
                         qed
                         finally show ?thesis .
                       qed
                     qed simp
                     moreover have "r \<in> {e \<in> ?r ` set (b # hs). 0 < e}"
                     proof (rule, rule, rule)
                       show "0 < r" by fact
                       show "a \<in> set (b#hs)" using Cons by simp
                       thus "r = ?r a" by auto
                     qed
                     ultimately show "nat r \<in> (\<Union>rel\<in>relations (set (b # hs)). nat ` {e \<in> rel ` set (b # hs). 0 < e})"
                       by fast
                   qed
                   moreover have "nat r < min_exp" using ot rq(2, 3) gr(4) by linarith
                   ultimately show False using le by fastforce
                 qed
               qed
               thus ?thesis using hs(4) Cons l by simp
             qed
             ultimately show ?thesis using lgA n dn by (metis card_length)
           qed
         qed
       qed (use dvot in blast)
     qed
   qed
 qed
 
 lemma (in comm_group) fundamental_subgr:
   fixes A :: "'a set"
   assumes "finite A" "A \<subseteq> carrier G"
   obtains gs where
     "set gs \<subseteq> generate G A" "distinct gs" "is_idirprod (generate G A) (\<lambda>g. generate G {g}) (set gs)"
     "successively (dvd) (map ord gs)" "card (set gs) \<le> card A"
   using assms ex_idirgen by meson
 
 text \<open>As every group is a subgroup of itself, the theorem follows directly. However, for reasons of
 convenience and uniqueness (although not completely proved), we strengthen the result by proving
 that the decomposition can be done without having the trivial factor in the product.
 We formulate the theorem in various ways: firstly, the invariant factor decomposition.\<close>
 
 theorem (in fin_gen_comm_group) invariant_factor_decomposition_idirprod:
   obtains gs where
     "set gs \<subseteq> carrier G" "distinct gs" "is_idirprod (carrier G) (\<lambda>g. generate G {g}) (set gs)"
     "successively (dvd) (map ord gs)" "card (set gs) \<le> card gen" "\<one> \<notin> set gs"
 proof -
   from fundamental_subgr[OF fin_gen gens_closed] obtain gs where
   gs: "set gs \<subseteq> carrier G" "distinct gs" "is_idirprod (carrier G) (\<lambda>g. generate G {g}) (set gs)"
     "successively (dvd) (map ord gs)" "card (set gs) \<le> card gen" using generators by auto
   hence cf: "compl_fam (\<lambda>g. generate G {g}) (set gs)" by simp
   let ?r = "remove1 \<one> gs"
   have r: "set ?r = set gs - {\<one>}" using gs by auto
   have "set ?r \<subseteq> carrier G" using gs by auto
   moreover have "distinct ?r" using gs by auto
   moreover have "is_idirprod (carrier G) (\<lambda>g. generate G {g}) (set ?r)"
   proof (intro is_idirprod_generate)
     show "set ?r \<subseteq> carrier G" using gs by auto
     show "compl_fam (\<lambda>g. generate G {g}) (set (remove1 \<one> gs))"
       by (rule compl_fam_generate_subset[OF cf gs(1)], use set_remove1_subset in fastforce)
     show "carrier G = generate G (set ?r)"
     proof -
       have "generate G (set ?r) = generate G (set gs)" using generate_one_irrel' r by simp
       with gs(3) show ?thesis by simp
     qed
   qed
   moreover have "successively (dvd) (map ord ?r)"
   proof (cases gs)
     case (Cons a list)
     have r: "(map ord (remove1 \<one> gs)) = remove1 1 (map ord gs)" using gs(1) 
     proof(induction gs)
       case (Cons a gs)
       hence "a \<in> carrier G" by simp
       with Cons ord_eq_1[OF this] show ?case by auto
     qed simp
     show ?thesis by (unfold r,
                      rule transp_successively_remove1[OF _ gs(4), unfolded transp_def],
                      auto)
   qed simp
   moreover have "card (set ?r) \<le> card gen" using gs(5) r
     by (metis List.finite_set card_Diff1_le dual_order.trans)
   moreover have "\<one> \<notin> set ?r" using gs(2) by auto
   ultimately show ?thesis using that by blast
 qed
 
 corollary (in fin_gen_comm_group) invariant_factor_decomposition_dirprod:
   obtains gs where
     "set gs \<subseteq> carrier G" "distinct gs"
     "DirProds (\<lambda>g. G\<lparr>carrier := generate G {g}\<rparr>) (set gs) \<cong> G"
     "successively (dvd) (map ord gs)" "card (set gs) \<le> card gen"
     "compl_fam (\<lambda>g. generate G {g}) (set gs)" "\<one> \<notin> set gs"
 proof -
   from invariant_factor_decomposition_idirprod obtain gs where
     gs: "set gs \<subseteq> carrier G" "distinct gs" "is_idirprod (carrier G) (\<lambda>g. generate G {g}) (set gs)"
         "successively (dvd) (map ord gs)" "card (set gs) \<le> card gen" "\<one> \<notin> set gs" by blast
   with cong_DirProds_IDirProds[OF gs(3)] gs 
   have "DirProds (\<lambda>g. G\<lparr>carrier := generate G {g}\<rparr>) (set gs) \<cong> G" by blast
   with gs that show ?thesis by auto
 qed
 
 corollary (in fin_gen_comm_group) invariant_factor_decomposition_dirprod_fam:
   obtains Hs where
     "\<And>H. H \<in> set Hs \<Longrightarrow> subgroup H G" "distinct Hs"
     "DirProds (\<lambda>H. G\<lparr>carrier := H\<rparr>) (set Hs) \<cong> G" "successively (dvd) (map card Hs)"
     "card (set Hs) \<le> card gen" "compl_fam id (set Hs)" "{\<one>} \<notin> set Hs"
 proof -
   from invariant_factor_decomposition_dirprod obtain gs where
   gs: "set gs \<subseteq> carrier G" "distinct gs"
       "DirProds (\<lambda>g. G\<lparr>carrier := generate G {g}\<rparr>) (set gs) \<cong> G"
       "successively (dvd) (map ord gs)" "card (set gs) \<le> card gen"
       "compl_fam (\<lambda>g. generate G {g}) (set gs)" "\<one> \<notin> set gs" by blast
   let ?gen = "(\<lambda>g. generate G {g})"
   let ?Hs = "map (\<lambda>g. ?gen g) gs"
   have "subgroup H G" if "H \<in> set ?Hs" for H using that gs by (auto intro: generate_is_subgroup)
   moreover have "distinct ?Hs"
     using compl_fam_imp_generate_inj[OF gs(1)] gs distinct_map by blast
   moreover have "DirProds (\<lambda>H. G\<lparr>carrier := H\<rparr>) (set ?Hs) \<cong> G"
   proof -
     have gg: "group (G\<lparr>carrier := ?gen g\<rparr>)" if "g \<in> set gs" for g
       by (use gs that in \<open>auto intro: subgroup.subgroup_is_group generate_is_subgroup\<close>)
     then interpret og: group "DirProds (\<lambda>g. G\<lparr>carrier := ?gen g\<rparr>) (set gs)"
       using DirProds_group_iff by blast
     have "DirProds (\<lambda>g. G\<lparr>carrier := ?gen g\<rparr>) (set gs) \<cong> DirProds (\<lambda>H. G\<lparr>carrier := H\<rparr>) (set ?Hs)"
     proof (intro DirProds_iso[of ?gen])
       show "bij_betw ?gen (set gs) (set ?Hs)"
         using \<open>distinct ?Hs\<close> gs(2) compl_fam_imp_generate_inj[OF gs(1, 6)]
         by (simp add: bij_betw_def)
       show "G\<lparr>carrier := ?gen g\<rparr> \<cong> G\<lparr>carrier := ?gen g\<rparr>" if "g \<in> set gs" for g by simp
       show "group (G\<lparr>carrier := ?gen g\<rparr>)" if "g \<in> set gs" for g using that by fact
       show "Group.group (G\<lparr>carrier := H\<rparr>)" if "H \<in> set ?Hs" for H
         by (use gs that in \<open>auto intro: subgroup.subgroup_is_group generate_is_subgroup\<close>)
     qed
     from group.iso_sym[OF og.is_group this] show ?thesis using gs iso_trans by blast
   qed
   moreover have "successively (dvd) (map card ?Hs)"
   proof -
     have "card (generate G {g}) = ord g" if "g \<in> set gs" for g
       using generate_pow_card that gs(1) by auto
     hence "map card ?Hs = map ord gs" by simp
     thus ?thesis using gs(4) by argo
   qed
   moreover have "card (set ?Hs) \<le> card gen" using gs
     by (metis \<open>distinct ?Hs\<close> distinct_card length_map)
   moreover have "compl_fam id (set ?Hs)"
     using compl_fam_cong[OF _ compl_fam_imp_generate_inj[OF gs(1, 6)], of id] using gs by auto
   moreover have "{\<one>} \<notin> set ?Hs" using generate_singleton_one gs by auto
   ultimately show ?thesis using that by blast
 qed
 
 text \<open>Here, the invariant factor decomposition in its classical form.\<close>
 
 corollary (in fin_gen_comm_group) invariant_factor_decomposition_Zn:
   obtains ns where
     "DirProds (\<lambda>n. Z (ns!n)) {..<length ns} \<cong> G" "successively (dvd) ns" "length ns \<le> card gen"
 proof -
   from invariant_factor_decomposition_dirprod obtain gs where
       gs: "set gs \<subseteq> carrier G" "distinct gs"
           "DirProds (\<lambda>g. G\<lparr>carrier := generate G {g}\<rparr>) (set gs) \<cong> G"
           "successively (dvd) (map ord gs)" "card (set gs) \<le> card gen"
           "compl_fam (\<lambda>g. generate G {g}) (set gs)" "\<one> \<notin> set gs" by blast
   let ?DP = "DirProds (\<lambda>g. G\<lparr>carrier := generate G {g}\<rparr>) (set gs)"
   have "\<exists>ns. DirProds (\<lambda>n. Z (ns!n)) {..<length ns} \<cong> G
            \<and> successively (dvd) ns \<and> length ns \<le> card gen"
   proof (cases gs, rule)
     case Nil
     from gs(3) Nil have co: "carrier ?DP = {\<one>\<^bsub>?DP\<^esub>}" unfolding DirProds_def by auto
     let ?ns = "[]"
     have "DirProds (\<lambda>n. Z ([] ! n)) {} \<cong> ?DP"
     proof(intro triv_iso DirProds_is_group)
       show "carrier (DirProds (\<lambda>n. Z ([] ! n)) {}) = {\<one>\<^bsub>DirProds (\<lambda>n. Z ([] ! n)) {}\<^esub>}"
         using DirProds_empty by blast
     qed (use co group_integer_mod_group Nil in auto)
     from that[of ?ns] gs co iso_trans[OF this gs(3)]
     show "DirProds (\<lambda>n. Z (?ns ! n)) {..<length ?ns} \<cong> G
         \<and> successively (dvd) ?ns \<and> length ?ns \<le> card gen"
       unfolding lessThan_def by simp
   next
     case c: (Cons a list)    
     let ?l = "map ord gs"
     from c have l: "length ?l > 0" by auto
     have "DirProds (\<lambda>n. Z (?l ! n)) {..<length ?l} \<cong> G"
     proof -
       have "DirProds (\<lambda>n. Z (?l ! n)) {..<length ?l} \<cong> ?DP"
       proof(intro DirProds_iso[where ?f = "\<lambda>n. gs!n"])
         show "bij_betw ((!) gs) {..<length ?l} (set gs)" using gs
           by (simp add: bij_betw_nth)
         show "Z (map ord gs ! i) \<cong> G\<lparr>carrier := generate G {gs ! i}\<rparr>" if "i \<in> {..<length ?l}" for i
         proof(rule group.iso_sym[OF subgroup.subgroup_is_group[OF generate_is_subgroup]
                    cyclic_group.Zn_iso[OF cyclic_groupI2]])
           show "order (G\<lparr>carrier := generate G {gs ! i}\<rparr>) = map ord gs ! i"
             unfolding order_def using that generate_pow_card[of "gs ! i"] gs(1) by force
         qed (use gs(1) that in auto)
         show "Group.group (Z (map ord gs ! i))" if "i \<in> {..<length (map ord gs)}" for i
           using group_integer_mod_group by blast
         show "Group.group (G\<lparr>carrier := generate G {g}\<rparr>)" if "g \<in> set gs" for g
           using that gs(1) subgroup.subgroup_is_group[OF generate_is_subgroup] by auto
       qed
       from iso_trans[OF this gs(3)] show ?thesis .
     qed
     moreover have "length ?l \<le> card gen" using gs by (metis distinct_card length_map)
     ultimately show ?thesis using gs c by fastforce
   qed
   thus ?thesis using that by blast
 qed
 
 text \<open>As every \<open>integer_mod_group\<close> can be decomposed into a product of prime power groups,
 we obtain (by using the fact that the direct product does not care about nestedness)
 the primary decomposition.\<close>
 
 lemma Zn_iso_DirProds_prime_powers:
   assumes "n \<noteq> 0"
   shows "Z n \<cong> DirProds (\<lambda>p. Z (p ^ multiplicity p n)) (prime_factors n)" (is "Z n \<cong> ?DP")
 proof (cases "n = 1")
   case True
   show ?thesis by (intro triv_iso[OF group_integer_mod_group DirProds_is_group],
                    use DirProds_empty carrier_integer_mod_group True in auto)
 next
   case nno: False
   interpret DP: group ?DP by (intro DirProds_is_group, use group_integer_mod_group in blast)
   have "order ?DP = prod (order \<circ> (\<lambda>p. Z (p ^ multiplicity p n))) (prime_factors n)"
     by (intro DirProds_order, blast)
   also have "\<dots> = prod (\<lambda>p. p ^ multiplicity p n) (prime_factors n)" using Zn_order by simp
   also have n: "\<dots> = n" using prod_prime_factors[OF assms] by simp
   finally have oDP: "order ?DP = n" .
   then interpret DP: finite_group ?DP
     by (unfold_locales, unfold order_def, metis assms card.infinite)
   let ?f = "\<lambda>p\<in>(prime_factors n). 1"
   have fc: "?f \<in> carrier ?DP"
   proof -
     have p: "0 < multiplicity p n" if "p \<in> prime_factors n" for p
       using prime_factors_multiplicity that by auto
     have pk: "1 < p ^ k" if "Factorial_Ring.prime p" "0 < k" for p k::nat
       using that one_less_power prime_gt_1_nat by blast
     show ?thesis unfolding DirProds_def PiE_def
       by(use carrier_integer_mod_group assms nno pk p in auto,
          metis in_prime_factors_iff nat_int of_nat_power one_less_nat_eq)
   qed
   have of: "DP.ord ?f = n"
   proof -
     have "n dvd j" if j: "?f [^]\<^bsub>?DP\<^esub> j = \<one>\<^bsub>?DP\<^esub>" for j
     proof (intro pairwise_coprime_dvd'[OF _ _ n[symmetric]])
       show "finite (prime_factors n)" by simp
       show "\<forall>a\<in>#prime_factorization n. a ^ multiplicity a n dvd j"
       proof 
         show "p ^ multiplicity p n dvd j" if "p \<in> prime_factors n" for p
         proof -
           from j have "(?f [^]\<^bsub>?DP\<^esub> j) p = 0"
             using that unfolding DirProds_def one_integer_mod_group by auto
           hence "?f p [^]\<^bsub>Z (p ^ multiplicity p n)\<^esub> j = 0" using comp_exp_nat[OF that] by metis
           hence "group.ord (Z (p ^ multiplicity p n)) (?f p) dvd j" using comp_in_carr[OF fc that]
             by (metis group.pow_eq_id group_integer_mod_group one_integer_mod_group)
           moreover have "group.ord (Z (p ^ multiplicity p n)) (?f p) = p ^ multiplicity p n"
             by (metis (no_types, lifting) Zn_neq1_cyclic_group Zn_order comp_in_carr
                                           cyclic_group.ord_gen_is_group_order fc integer_mod_group_1
                                           restrict_apply' that)
           ultimately show ?thesis by simp
         qed
       qed
       show "coprime (i ^ multiplicity i n) (j ^ multiplicity j n)"
         if "i \<in># prime_factorization n" "j \<in># prime_factorization n" "i \<noteq> j" for i j
         using that diff_prime_power_imp_coprime by blast
     qed
     thus ?thesis using fc DP.ord_dvd_group_order gcd_nat.asym oDP by force
   qed
   interpret DP: cyclic_group ?DP ?f by (intro DP.element_ord_generates_cyclic, use of oDP fc in auto)
   show ?thesis using DP.iso_sym[OF DP.Zn_iso[OF oDP]] .
 qed
 
 lemma Zn_iso_DirProds_prime_powers':
   assumes "n \<noteq> 0"
   shows "Z n \<cong> DirProds (\<lambda>p. Z p) ((\<lambda>p. p ^ multiplicity p n) ` (prime_factors n))" (is "Z n \<cong> ?DP")
 proof -
   have cp: "(\<lambda>p. Z (p ^ multiplicity p n)) = (\<lambda>p. Z p) \<circ> (\<lambda>p. p ^ multiplicity p n)" by auto
   have "DirProds (\<lambda>p. Z (p ^ multiplicity p n)) (prime_factors n) \<cong> ?DP"
   proof(subst cp, intro DirProds_iso2)
     show "inj_on (\<lambda>p. p ^ multiplicity p n) (prime_factors n)"
       by (intro inj_onI; simp add: prime_factors_multiplicity prime_power_inj'')
     show "group (DirProds Z ((\<lambda>p. p ^ multiplicity p n) ` prime_factors n))"
       by (intro DirProds_is_group, use group_integer_mod_group in auto)
   qed
   with Zn_iso_DirProds_prime_powers[OF assms] show ?thesis using Group.iso_trans by blast
 qed
 
 corollary (in fin_gen_comm_group) primary_decomposition_Zn:
   obtains ns where
     "DirProds (\<lambda>n. Z (ns!n)) {..<length ns} \<cong> G"
     "\<forall>n\<in>set ns. n = 0 \<or> (\<exists>p k. Factorial_Ring.prime p \<and> k > 0 \<and> n = p ^ k)"
 proof -
   from invariant_factor_decomposition_Zn obtain ms where
     ms: "DirProds (\<lambda>m. Z (ms!m)) {..<length ms} \<cong> G" "successively (dvd) ms" "length ms \<le> card gen"
     by blast
   let ?I = "{..<length ms}"
   let ?J = "\<lambda>i. if ms!i = 0 then {0} else (\<lambda>p. p ^ multiplicity p (ms!i)) ` (prime_factors (ms!i))"
   let ?G = "\<lambda>i. Z"
   let ?f = "\<lambda>i. DirProds (?G i) (?J i)"
   have "DirProds (\<lambda>m. Z (ms!m)) {..<length ms} \<cong> DirProds ?f {..<length ms}"
   proof (intro DirProds_iso[of id])
     show "bij_betw id {..<length ms} {..<length ms}" by blast
     show "Z (ms ! i) \<cong> ?f (id i)" if "i \<in> {..<length ms}" for i
       by (cases "ms!i = 0",
           simp add: DirProds_one_cong_sym,
           auto intro: Zn_iso_DirProds_prime_powers')
     show "\<And>i. i \<in> {..<length ms} \<Longrightarrow> group (Z (ms ! i))" by auto
     show "group (?f j)" if "j \<in> {..<length ms}" for j by (auto intro: DirProds_is_group)
   qed
   also have "\<dots> \<cong> DirProds (\<lambda>(i,j). ?G i j) (Sigma ?I ?J)"
     by(rule DirProds_Sigma)
   finally have G1: "G \<cong> DirProds (\<lambda>(i,j). ?G i j) (Sigma ?I ?J)" using ms(1)
     by (metis (no_types, lifting) DirProds_is_group Group.iso_trans group.iso_sym group_integer_mod_group)
   have "\<exists>ps. set ps = Sigma ?I ?J \<and> distinct ps" by(intro finite_distinct_list, auto)
   then obtain ps where ps: "set ps = Sigma ?I ?J" "distinct ps" by blast
   define ns where ns: "ns = map snd ps"
   have "DirProds (\<lambda>n. Z (ns!n)) {..<length ns} \<cong> DirProds (\<lambda>(i,j). ?G i j) (Sigma ?I ?J)"
   proof -
     obtain b::"nat \<Rightarrow> (nat \<times> nat)"
       where b: "\<forall>i<length ns. ns!i = snd (b i)" "bij_betw b {..<length ns} (Sigma ?I ?J)"
       using ns ps bij_betw_nth by fastforce
     moreover have "Z (ns ! i) \<cong> (case b i of (i, x) \<Rightarrow> Z x)" if "i \<in> {..<length ns}" for i
     proof -
       have "ns ! i = snd (b i)" using b that by blast
       thus ?thesis by (simp add: case_prod_beta)
     qed
     ultimately show ?thesis by (auto intro: DirProds_iso)
   qed
   with G1 have "DirProds (\<lambda>n. Z (ns!n)) {..<length ns} \<cong> G" using Group.iso_trans iso_sym by blast
   moreover have "n = 0 \<or> (\<exists>p k. Factorial_Ring.prime p \<and> k > 0 \<and> n = p ^ k)" if "n\<in>set ns" for n
   proof -
     have "k = 0 \<or> (\<exists>p\<in>prime_factors (ms!i). k = p ^ multiplicity p (ms!i))" if "k \<in> ?J i" for k i
       by (cases "ms!i = 0", use that in auto)
     with that ns ps show ?thesis
       by (auto, metis (no_types, lifting) mem_Collect_eq neq0_conv prime_factors_multiplicity)
   qed
   ultimately show
   "(\<And>ns. \<lbrakk>DirProds (\<lambda>n. Z (ns ! n)) {..<length ns} \<cong> G;
           \<forall>n\<in>set ns. n = 0 \<or> (\<exists>p k. Factorial_Ring.prime p \<and> k > 0 \<and> n = p ^ k)\<rbrakk> \<Longrightarrow> thesis)
     \<Longrightarrow> thesis" by blast
 qed
 
 text \<open>As every finite group is also finitely generated, it follows that a finite group can be
 decomposed in a product of finite cyclic groups.\<close>
 
 lemma (in finite_comm_group) cyclic_product:
   obtains ns where "DirProds (\<lambda>n. Z (ns!n)) {..<length ns} \<cong> G" "\<forall>n\<in>set ns. n\<noteq>0"
 proof -
   from primary_decomposition_Zn obtain ns where
     ns: "DirProds (\<lambda>n. Z (ns ! n)) {..<length ns} \<cong> G"
         "\<forall>n\<in>set ns. n = 0 \<or> (\<exists>p k. normalization_semidom_class.prime p \<and> 0 < k \<and> n = p ^ k)"
     by blast
   have "False" if "n \<in> {..<length ns}" "ns!n = 0" for n
   proof -
     from that have "order (DirProds (\<lambda>n. Z (ns ! n)) {..<length ns}) = 0"
       using DirProds_order[of "{..<length ns}" "\<lambda>n. Z (ns!n)"] Zn_order by auto
     with fin iso_same_card[OF ns(1)] show False unfolding order_def by auto
   qed
   hence "\<forall>n\<in>set ns. n\<noteq>0"
     by (metis in_set_conv_nth lessThan_iff)
   with ns show ?thesis using that by blast
 qed
 
 no_notation integer_mod_group ("Z")
 
 end
diff --git a/thys/Finitely_Generated_Abelian_Groups/General_Auxiliary.thy b/thys/Finitely_Generated_Abelian_Groups/General_Auxiliary.thy
--- a/thys/Finitely_Generated_Abelian_Groups/General_Auxiliary.thy
+++ b/thys/Finitely_Generated_Abelian_Groups/General_Auxiliary.thy
@@ -1,270 +1,272 @@
 (*
     File:     General_Auxiliary.thy
     Author:   Joseph Thommes, TU München; Manuel Eberl, TU München
 *)
 section \<open>Auxiliary lemmas\<close>
 
 theory General_Auxiliary
-  imports "HOL-Algebra.Algebra"
+  imports Complex_Main
+          "HOL-Algebra.IntRing"
+          "HOL.Rings"
 begin
 
 lemma inter_imp_subset: "A \<inter> B = A \<Longrightarrow> A \<subseteq> B"
   by blast
 
 lemma card_inter_eq:
   assumes "finite A" "card (A \<inter> B) = card A"
   shows "A \<subseteq> B"
 proof -
   have "A \<inter> B \<subseteq> A" by blast
   with assms have "A \<inter> B = A" using card_subset_eq by blast
   thus ?thesis by blast
 qed
 
 lemma coprime_eq_empty_prime_inter:
   assumes "(n::nat) \<noteq> 0" "m \<noteq> 0"
   shows "coprime n m \<longleftrightarrow> (prime_factors n) \<inter> (prime_factors m) = {}"
 proof
   show "coprime n m \<Longrightarrow> prime_factors n \<inter> prime_factors m = {}"
   proof (rule ccontr)
     assume cp: "coprime n m"
     assume pf: "prime_factors n \<inter> prime_factors m \<noteq> {}"
     then obtain p where p: "p \<in> prime_factors n" "p \<in> prime_factors m" by blast
     then have p_dvd: "p dvd n" "p dvd m" by blast+
     moreover have "\<not>is_unit p" using p using not_prime_unit by blast
     ultimately show "False" using cp unfolding coprime_def by simp
   qed
   assume assm: "prime_factors n \<inter> prime_factors m = {}"
   show "coprime n m" unfolding coprime_def
   proof
     fix c
     show "c dvd n \<longrightarrow> c dvd m \<longrightarrow> is_unit c"
     proof(rule; rule)
       assume c: "c dvd n" "c dvd m"
       then have "prime_factors c \<subseteq> prime_factors n" "prime_factors c \<subseteq> prime_factors m"
         using assms dvd_prime_factors by blast+
       then have "prime_factors c = {}" using assm by blast
       thus "is_unit c" using assms c
         by (metis dvd_0_left_iff prime_factorization_empty_iff set_mset_eq_empty_iff)
     qed
   qed
 qed
 
 lemma prime_factors_Prod:
   assumes "finite S" "\<And>a. a \<in> S \<Longrightarrow> f a \<noteq> 0"
   shows "prime_factors (prod f S) = \<Union>(prime_factors ` f ` S)"
   using assms
 proof(induction S rule: finite_induct)
   case empty
   then show ?case by simp
 next
   case i: (insert x F)
   from i have x: "f x \<noteq> 0" by blast
   from i have F: "prod f F \<noteq> 0" by simp
   from i have "prime_factors(prod f F) = \<Union> (prime_factors ` f ` F)" by blast
   moreover have "prod f (insert x F) = (prod f F) * f x" using i mult.commute by force
   ultimately
   have "prime_factors (prod f (insert x F)) = (\<Union>(prime_factors ` f ` F)) \<union> prime_factors (f x)"
     using prime_factors_product[OF F x] by argo
   thus ?case by force
 qed
 
 lemma lcm_is_Min_multiple_nat:
   assumes "c \<noteq> 0" "(a::nat) dvd c" "(b::nat) dvd c"
   shows "c \<ge> lcm a b"
   using lcm_least[of a c b] assms by fastforce
 
 lemma diff_prime_power_imp_coprime:
   assumes "p \<noteq> q" "Factorial_Ring.prime (p::nat)" "Factorial_Ring.prime q"
   shows "coprime (p ^ (n::nat)) (q ^ m)"
   using assms
   by (metis power_0 power_one_right prime_dvd_power prime_imp_power_coprime_nat
             prime_nat_iff prime_power_inj'')
 
 lemma "finite (prime_factors x)"
   using finite_set_mset by blast
 
 lemma card_ge_1_two_diff:
   assumes "card A > 1"
   obtains x y where "x \<in> A" "y \<in> A" "x \<noteq> y"
 proof -
   have fA: "finite A" using assms by (metis card.infinite not_one_less_zero)
   from assms obtain x where x: "x \<in> A" by fastforce
   with assms fA have "card (A - {x}) > 0" by simp
   then obtain y where y: "y \<in> (A - {x})" by (metis card_gt_0_iff ex_in_conv)
   thus ?thesis using that[of x y] x by blast
 qed
 
 lemma infinite_two_diff:
   assumes "infinite A"
   obtains x y where "x \<in> A" "y \<in> A" "x \<noteq> y"
 proof -
   from assms obtain x where x: "x \<in> A" by fastforce
   from assms have "infinite (A - {x})" by simp
   then obtain y where y: "y \<in> (A - {x})"
     by (metis ex_in_conv finite.emptyI)
   show ?thesis using that[of x y] using x y by blast
 qed
 
 lemma Inf_le:
   "Inf A \<le> x" if "x \<in> (A::nat set)" for x
 proof (cases "A = {}")
   case True
   then show ?thesis using that by simp
 next
   case False
   hence "Inf A \<le> Inf {x}" using that by (simp add: cInf_lower)
   also have "\<dots> = x" by simp
   finally show "Inf A \<le> x" by blast
 qed
 
 lemma switch_elem_card_le:
   assumes "a \<in> A"
   shows "card (A - {a} \<union> {b}) \<le> card A"
   using assms
   by (metis Diff_insert_absorb Set.set_insert Un_commute card.infinite card_insert_disjoint
             card_mono finite_insert insert_is_Un insert_subset order_refl)
 
 lemma pairwise_coprime_dvd:
   assumes "finite A" "pairwise coprime A" "(n::nat) = prod id A" "\<forall>a\<in>A. a dvd j"
   shows "n dvd j"
   using assms
 proof (induction A arbitrary: n)
   case i: (insert x F)
   have "prod id F dvd j" "x dvd j" using i unfolding pairwise_def by auto
   moreover have "coprime (prod id F) x"
     by (metis i(2, 4) id_apply pairwise_insert prod_coprime_left)
   ultimately show ?case using i(1, 2, 5) by (simp add: coprime_commute divides_mult)
 qed simp
 
 lemma pairwise_coprime_dvd':
   assumes "finite A" "\<And>i j. \<lbrakk>i \<in> A; j \<in> A; i \<noteq> j\<rbrakk> \<Longrightarrow> coprime (f i) (f j)"
           "(n::nat) = prod f A" "\<forall>a\<in>A. f a dvd j"
   shows "n dvd j"
   using assms
 proof (induction A arbitrary: n)
   case i: (insert x F)
   have "prod f F dvd j" "f x dvd j" using i unfolding pairwise_def by auto
   moreover have "coprime (prod f F) (f x)" by(intro prod_coprime_left, use i in blast)
   ultimately show ?case using i by (simp add: coprime_commute divides_mult)
 qed simp
 
 lemma transp_successively_remove1:
   assumes "transp f" "successively f l"
   shows "successively f (remove1 a l)" using assms(2)
 proof(induction l rule: induct_list012)
   case (3 x y zs)
   from 3(3)[unfolded successively.simps] have fs: "f x y" "successively f (y # zs)" by auto
   moreover from this(2) successively.simps have s: "successively f zs" by(cases zs, auto)
   ultimately have s2: "successively f (remove1 a zs)" "successively f (remove1 a (y # zs))"
     using 3 by auto
   consider (x) "x = a" | (y) "y = a \<and> x \<noteq> a" | (zs) "a \<noteq> x \<and> a \<noteq> y" by blast
   thus ?case
   proof (cases)
     case x
     then show ?thesis using 3 by simp
   next
     case y
     then show ?thesis
     proof (cases zs)
       case Nil
       then show ?thesis using fs by simp
     next
       case (Cons a list)
       hence "f y a" using fs by simp
       hence "f x a" using fs(1) assms(1)[unfolded transp_def] by blast
       then show ?thesis using Cons y s by auto
     qed
   next
     case zs
     then show ?thesis using s2 fs by auto
   qed
 qed auto
 
 
 lemma exp_one_2pi_iff:
   fixes x::real shows "exp (2 * of_real pi * \<i> * x) = 1 \<longleftrightarrow> x \<in> \<int>"
 proof -
   have c: "cis (2 * x * pi) = 1 \<longleftrightarrow> x \<in> \<int>"
     by (auto simp: complex_eq_iff sin_times_pi_eq_0 cos_one_2pi_int, meson Ints_cases)
   have "exp (2 * of_real pi * \<i> * x) = exp (\<i> * complex_of_real (2 * x * pi))"
   proof -
     have "2 * of_real pi * \<i> * x = \<i> * complex_of_real (2 * x * pi)" by simp
     thus ?thesis by argo
   qed
   also from cis_conv_exp have "\<dots> = cis (2 * x * pi)" by simp
   finally show ?thesis using c by simp
 qed
 
 (* Manuel Eberl *)
 lemma of_int_divide_in_Ints_iff:
   assumes "b \<noteq> 0"
   shows   "(of_int a / of_int b :: 'a :: field_char_0) \<in> \<int> \<longleftrightarrow> b dvd a"
 proof
   assume *: "(of_int a / of_int b :: 'a :: field_char_0) \<in> \<int>"
   from * obtain n where "of_int a / of_int b = (of_int n :: 'a)"
     by (elim Ints_cases)
   hence "of_int (b * n) = (of_int a :: 'a)"
     using assms by (subst of_int_mult) (auto simp: field_simps)
   hence "b * n = a"
     by (subst (asm) of_int_eq_iff)
   thus "b dvd a" by auto
 qed auto
 
 (* Manuel Eberl *)
 lemma of_nat_divide_in_Ints_iff:
   assumes "b \<noteq> 0"
   shows   "(of_nat a / of_nat b :: 'a :: field_char_0) \<in> \<int> \<longleftrightarrow> b dvd a"
   using of_int_divide_in_Ints_iff[of "int b" "int a"] assms by simp
 
 lemma true_nth_unity_root:
   fixes n::nat
   obtains x::complex where "x ^ n = 1" "\<And>m. \<lbrakk>0<m; m<n\<rbrakk> \<Longrightarrow> x ^ m \<noteq> 1"
 proof(cases "n = 0")
   case False
   show ?thesis
   proof (rule that)
     show "cis (2 * pi / n) ^ n = 1"
       by (simp add: DeMoivre)
   next
     fix m assume m: "m > 0" "m < n"
     have "cis (2 * pi / n) ^ m = cis (2 * pi * m / n)"
       by (simp add: DeMoivre algebra_simps)
     also have "\<dots> = 1 \<longleftrightarrow> real m / real n \<in> \<int>"
       using exp_one_2pi_iff[of "m / n"] by (simp add: cis_conv_exp algebra_simps)
     also have "\<dots> \<longleftrightarrow> n dvd m"
       using m by (subst of_nat_divide_in_Ints_iff) auto
     also have "\<not>n dvd m"
       using m by auto
     finally show "cis (2 * pi / real n) ^ m \<noteq> 1" .
   qed
 qed simp
 
 lemma finite_bij_betwI:
   assumes "finite A" "finite B" "inj_on f A" "f \<in> A \<rightarrow> B" "card A = card B"
   shows "bij_betw f A B"
 proof (intro bij_betw_imageI)
   show "inj_on f A" by fact
   show "f ` A = B"
   proof -
     have "card (f ` A) = card B" using assms by (simp add: card_image)
     moreover have "f ` A \<subseteq> B" using assms by blast
     ultimately show ?thesis using assms by (meson card_subset_eq)
   qed
 qed
 
 lemma powi_mod:
   "x powi m = x powi (m mod n)" if "x ^ n = 1" "n > 0" for x::complex and m::int
 proof -
   have xnz: "x \<noteq> 0" using that by (metis zero_neq_one zero_power)
   obtain k::int where k: "m = k*n + (m mod n)" using div_mod_decomp_int by blast
   have "x powi m = x powi (k*n) * x powi (m mod n)" by (subst k, intro power_int_add, use xnz in auto)
   moreover have "x powi (k*n) = 1" using that
     by (metis mult.commute power_int_1_left power_int_mult power_int_of_nat)
   ultimately show ?thesis by force
 qed
 
 (* Manuel Eberl *)
 lemma Sigma_insert: "Sigma (insert x A) B = (\<lambda>y. (x, y)) ` B x \<union> Sigma A B"
   by auto
 
 end
\ No newline at end of file
diff --git a/thys/Finitely_Generated_Abelian_Groups/Generated_Groups_Extend.thy b/thys/Finitely_Generated_Abelian_Groups/Generated_Groups_Extend.thy
--- a/thys/Finitely_Generated_Abelian_Groups/Generated_Groups_Extend.thy
+++ b/thys/Finitely_Generated_Abelian_Groups/Generated_Groups_Extend.thy
@@ -1,238 +1,238 @@
 (*
     File:     Generated_Groups_Extend.thy
     Author:   Joseph Thommes, TU München
 *)
 section \<open>Generated Groups\<close>
 
 theory Generated_Groups_Extend
-  imports Miscellaneous_Groups "HOL-Algebra.Algebra"
+  imports Miscellaneous_Groups
 begin
 
 text \<open>This section extends the lemmas and facts about \<open>generate\<close>. Starting with a basic fact.\<close>
 
 lemma (in group) generate_sincl:
   "A \<subseteq> generate G A"
   using generate.incl by fast
 
 text \<open>The following lemmas reflect some of the idempotence characteristics of \<open>generate\<close> and have
 proved useful at several occasions.\<close>
 
 lemma (in group) generate_idem:
   assumes "A \<subseteq> carrier G"
   shows "generate G (generate G A) = generate G A"
   using assms generateI group.generate_is_subgroup by blast
 
 lemma (in group) generate_idem':
   assumes "A \<subseteq> carrier G" "B \<subseteq> carrier G"
   shows "generate G (generate G A \<union> B) = generate G (A \<union> B)"
 proof
   show "generate G (generate G A \<union> B) \<subseteq> generate G (A \<union> B)"
   proof -
     have "generate G A \<union> B \<subseteq> generate G (A \<union> B)"
     proof -
       have "generate G A \<subseteq> generate G (A \<union> B)" using mono_generate by simp
       moreover have "B \<subseteq> generate G (A \<union> B)" by (simp add: generate.incl subset_iff)
       ultimately show ?thesis by simp
     qed
     then have "generate G (generate G A \<union> B) \<subseteq> generate G (generate G (A \<union> B))"
       using mono_generate by auto
     with generate_idem[of "A \<union> B"] show ?thesis using assms by simp
   qed
   show "generate G (A \<union> B) \<subseteq> generate G (generate G A \<union> B)"
   proof -
     have "A \<subseteq> generate G A" using generate.incl by fast
     thus ?thesis using mono_generate[of "A \<union> B" "generate G A \<union> B"] by blast
   qed
 qed
 
 lemma (in group) generate_idem'_right:
   assumes "A \<subseteq> carrier G" "B \<subseteq> carrier G"
   shows "generate G (A \<union> generate G B) = generate G (A \<union> B)"
   using generate_idem'[OF assms(2) assms(1)] by (simp add: sup_commute)
 
 lemma (in group) generate_idem_Un:
   assumes "A \<subseteq> carrier G"
   shows "generate G (\<Union>x\<in>A. generate G {x}) = generate G A"
 proof
   have "A \<subseteq> (\<Union>x\<in>A. generate G {x})" using generate.incl by force
   thus "generate G A \<subseteq> generate G (\<Union>x\<in>A. generate G {x})" using mono_generate by presburger
   have "\<And>x. x \<in> A \<Longrightarrow> generate G {x} \<subseteq> generate G A" using mono_generate by auto
   hence "(\<Union>x\<in>A. generate G {x}) \<subseteq> generate G A" by blast
   thus "generate G (\<Union>x\<in>A. generate G {x}) \<subseteq> generate G A"
     using generate_idem[OF assms] mono_generate by blast
 qed
 
 lemma (in group) generate_idem_fUn:
   assumes "f A \<subseteq> carrier G"
   shows "generate G (\<Union> {generate G {x} |x. x \<in> f A}) = generate G (f A)"
 proof
   have "f A \<subseteq> \<Union> {generate G {x} |x. x \<in> f A}"
   proof
     fix x
     assume x: "x \<in> f A"
     have "x \<in> generate G {x}" using generate.incl by fast
     thus "x \<in> \<Union> {generate G {x} |x. x \<in> f A}" using x by blast
   qed
   thus "generate G (f A) \<subseteq> generate G (\<Union> {generate G {x} |x. x \<in> f A})" using mono_generate by auto
   have "\<And>x. x \<in> f A \<Longrightarrow> generate G {x} \<subseteq> generate G (f A)" using mono_generate by simp
   hence "(\<Union> {generate G {x} |x. x \<in> f A}) \<subseteq> generate G (f A)" by blast
   with mono_generate[OF this] show "generate G (\<Union> {generate G {x} |x. x \<in> f A}) \<subseteq> generate G (f A)"
     using generate_idem[OF assms] by simp
 qed
 
 lemma (in group) generate_idem_fim_Un:
   assumes "\<Union>(f ` A) \<subseteq> carrier G"
   shows "generate G (\<Union>S \<in> A. generate G (f S)) = generate G (\<Union> {generate G {x} |x. x \<in> \<Union> (f ` A)})"
 proof
   
   have "\<And>S. S \<in> A \<Longrightarrow> generate G (f S) = generate G (\<Union> {generate G {x} |x. x \<in> f S})"
     using generate_idem_fUn[of f] assms by blast
   then have "generate G (\<Union>S \<in> A. generate G (f S))
            = generate G (\<Union>S \<in> A. generate G (\<Union> {generate G {x} |x. x \<in> f S}))" by simp
 
   have "\<Union> {generate G {x} |x. x \<in> \<Union> (f ` A)} \<subseteq> (\<Union>S\<in>A. generate G (f S))"
   proof
     fix x
     assume x: "x \<in> \<Union> {generate G {x} |x. x \<in> \<Union> (f ` A)}"
     then obtain a where a: "x \<in> generate G {a}" "a \<in> \<Union> (f ` A)" by blast
     then obtain M where M: "a \<in> f M" "M \<in> A" by blast
     then have "generate G {a} \<subseteq> generate G (f M)"
       using generate.incl[OF M(1), of G] mono_generate[of "{a}" "generate G (f M)"]
             generate_idem assms by auto
     then have "x \<in> generate G (f M)" using a by blast
     thus "x \<in> (\<Union>S\<in>A. generate G (f S))" using M by blast
   qed
   thus "generate G (\<Union> {generate G {x} |x. x \<in> \<Union> (f ` A)}) \<subseteq> generate G (\<Union>S\<in>A. generate G (f S))"
     using mono_generate by simp
   have a: "generate G (\<Union>S\<in>A. generate G (f S)) \<subseteq> generate G (\<Union> (f ` A))"
   proof -
     have "\<And>S. S \<in> A \<Longrightarrow> generate G (f S) \<subseteq> generate G (\<Union> (f ` A))"
       using mono_generate[of _ "\<Union> (f ` A)"] by blast
     then have "(\<Union>S\<in>A. generate G (f S)) \<subseteq> generate G (\<Union> (f ` A))" by blast
     then have "generate G (\<Union>S\<in>A. generate G (f S)) \<subseteq> generate G (generate G (\<Union> (f ` A)))"
       using mono_generate by meson
     thus "generate G (\<Union>S\<in>A. generate G (f S)) \<subseteq>  generate G (\<Union> (f ` A))"
       using generate_idem assms by blast
   qed
   have "\<Union> {generate G {x} |x. x \<in> \<Union> (f ` A)} = (\<Union>x\<in>\<Union> (f ` A). generate G {x})" by blast
   with generate_idem_Un[OF assms]
   have "generate G (\<Union> {generate G {x} |x. x \<in> \<Union> (f ` A)}) = generate G (\<Union> (f ` A))" by simp
   with a show "generate G (\<Union>S\<in>A. generate G (f S))
              \<subseteq> generate G (\<Union> {generate G {x} |x. x \<in> \<Union> (f ` A)})" by blast
 qed
 
 text \<open>The following two rules allow for convenient proving of the equality of two generated sets.\<close>
 
 lemma (in group) generate_eqI:
   assumes "A \<subseteq> carrier G" "B \<subseteq> carrier G" "A \<subseteq> generate G B" "B \<subseteq> generate G A"
   shows "generate G A = generate G B"
   using assms generate_idem by (metis generate_idem' inf_sup_aci(5) sup.absorb2)
 
 lemma (in group) generate_one_switched_eqI:
   assumes "A \<subseteq> carrier G" "a \<in> A" "B = (A - {a}) \<union> {b}"
   and "b \<in> generate G A" "a \<in> generate G B"
   shows "generate G A = generate G B"
 proof(intro generate_eqI)
   show "A \<subseteq> carrier G" by fact
   show "B \<subseteq> carrier G" using assms generate_incl by blast
   show "A \<subseteq> generate G B" using assms generate_sincl[of B] by blast
   show "B \<subseteq> generate G A" using assms generate_sincl[of A] by blast
 qed
 
 lemma (in group) generate_subset_eqI:
   assumes "A \<subseteq> carrier G" "B \<subseteq> A" "A - B \<subseteq> generate G B"
   shows "generate G A = generate G B"
 proof
   show "generate G B \<subseteq> generate G A" by (intro mono_generate, fact)
   show "generate G A \<subseteq> generate G B"
   proof(subst generate_idem[of "B", symmetric])
     show "generate G A \<subseteq> generate G (generate G B)"
       by (intro mono_generate, use assms generate_sincl[of B] in auto)
   qed (use assms in blast)
 qed
 
 text \<open>Some smaller lemmas about \<open>generate\<close>.\<close>
 
 lemma (in group) generate_subset_change_eqI:
   assumes "A \<subseteq> carrier G" "B \<subseteq> carrier G" "C \<subseteq> carrier G" "generate G A = generate G B"
   shows "generate G (A \<union> C) = generate G (B \<union> C)"
   by (metis assms generate_idem')
 
 lemma (in group) generate_subgroup_id:
   assumes "subgroup H G"
   shows "generate G H = H"
   using assms generateI by auto
 
 lemma (in group) generate_consistent':
   assumes "subgroup H G" "A \<subseteq> H"
   shows "\<forall>x \<in> A. generate G {x} = generate (G\<lparr>carrier := H\<rparr>) {x}"
   using generate_consistent assms by auto
 
 lemma (in group) generate_singleton_one:
   assumes "generate G {a} = {\<one>}"
   shows "a = \<one>"
   using generate.incl[of a "{a}" G] assms by auto
 
 lemma (in group) generate_inv_eq:
   assumes "a \<in> carrier G"
   shows "generate G {a} = generate G {inv a}"
   by (intro generate_eqI;
       use assms generate.inv[of a] generate.inv[of "inv a" "{inv a}" G] inv_inv[OF assms] in auto)
 
 lemma (in group) generate_eq_imp_subset:
   assumes "generate G A = generate G B"
   shows "A \<subseteq> generate G B"
   using generate.incl assms by fast
 
 
 text \<open>The neutral element does not play a role when generating a subgroup.\<close>
 
 lemma (in group) generate_one_irrel:
   "generate G A = generate G (A \<union> {\<one>})"
 proof
   show "generate G A \<subseteq> generate G (A \<union> {\<one>})" by (intro mono_generate, blast)
   show "generate G (A \<union> {\<one>}) \<subseteq> generate G A"
   proof(rule subsetI)
     show "x \<in> generate G A" if "x \<in> generate G (A \<union> {\<one>})" for x using that
       by (induction rule: generate.induct;
           use generate.one generate.incl generate.inv generate.eng in auto)
   qed
 qed
 
 lemma (in group) generate_one_irrel':
   "generate G A = generate G (A - {\<one>})"
   using generate_one_irrel by (metis Un_Diff_cancel2)
 
 text \<open>Also, we can express the subgroup generated by a singleton with finite order using just its
 powers up to its order.\<close>
 
 lemma (in group) generate_nat_pow:
   assumes "ord a \<noteq> 0" "a \<in> carrier G"
   shows "generate G {a} = {a [^] k |k. k \<in> {0..ord a - 1}}"
   using assms generate_pow_nat ord_elems_inf_carrier by auto
 
 lemma (in group) generate_nat_pow':
   assumes "ord a \<noteq> 0" "a \<in> carrier G"
   shows "generate G {a} = {a [^] k |k. k \<in> {1..ord a}}"
 proof -
   have "{a [^] k |k. k \<in> {1..ord a}} = {a [^] k |k. k \<in> {0..ord a - 1}}"
   proof -
     have "a [^] k \<in> {a [^] k |k. k \<in> {0..ord a - 1}}" if "k \<in> {1..ord a}" for k
       using that pow_nat_mod_ord[OF assms(2, 1), of "ord a"] assms by (cases "k = ord a"; force)
     moreover have "a [^] k \<in> {a [^] k |k. k \<in> {1..ord a}}" if "k \<in> {0..ord a - 1}" for k
     proof(cases "k = 0")
       case True
       hence "a [^] k = a [^] ord a" using pow_ord_eq_1[OF assms(2)] by auto
       moreover have "ord a \<in> {1..ord a}"
         using assms unfolding atLeastAtMost_def atLeast_def atMost_def by auto
       ultimately show ?thesis by blast
     next
       case False
       then show ?thesis using that by auto
     qed 
     ultimately show ?thesis by blast
   qed
   with generate_nat_pow[OF assms] show ?thesis by simp
 qed
 
 end
\ No newline at end of file
diff --git a/thys/Finitely_Generated_Abelian_Groups/Group_Relations.thy b/thys/Finitely_Generated_Abelian_Groups/Group_Relations.thy
--- a/thys/Finitely_Generated_Abelian_Groups/Group_Relations.thy
+++ b/thys/Finitely_Generated_Abelian_Groups/Group_Relations.thy
@@ -1,222 +1,222 @@
 (*
     File:     Group_Relations.thy
     Author:   Joseph Thommes, TU München
 *)
 section \<open>Group relations\<close>
 
 theory Group_Relations
   imports Finite_Product_Extend
 begin
 
 text \<open>We introduce the notion of a relation of a set of elements: a way to express the neutral
 element by using only powers of said elements. The following predicate describes the set of all the
 relations that one can construct from a set of elements.\<close>
 
 definition (in comm_group) relations :: "'a set \<Rightarrow> ('a \<Rightarrow> int) set" where
   "relations A = {f. finprod G (\<lambda>a. a [^] f a) A = \<one>} \<inter> extensional A"
 
 text \<open>Now some basic lemmas about relations.\<close>
 
 lemma (in comm_group) in_relationsI[intro]:
   assumes "finprod G (\<lambda>a. a [^] f a) A = \<one>" "f \<in> extensional A"
   shows "f \<in> relations A"
   unfolding relations_def using assms by blast
 
 lemma (in comm_group) triv_rel:
   "restrict (\<lambda>_. 0::int) A \<in> relations A"
 proof
   show "(\<Otimes>a\<in>A. a [^] (\<lambda>_\<in>A. 0::int) a) = \<one>" by (intro finprod_one_eqI, simp)
 qed simp
 
 lemma (in comm_group) not_triv_relI:
   assumes "a \<in> A" "f a \<noteq> (0::int)"
   shows "f \<noteq> (\<lambda>_\<in>A. 0::int)"
   using assms by auto
 
 lemma (in comm_group) rel_in_carr:
   assumes "A \<subseteq> carrier G" "r \<in> relations A"
   shows "(\<lambda>a. a [^] r a) \<in> A \<rightarrow> carrier G"
   by (meson Pi_I assms(1) int_pow_closed subsetD)
 
 text \<open>The following lemmas are of importance when proving the fundamental theorem of finitely
 generated abelian groups in the case that there is just the trivial relation between a set of
 generators. They all build up to the last lemma that then is actually used in the proof.\<close>
 
 lemma (in comm_group) relations_zero_imp_pow_not_one:
   assumes "a \<in> A" "\<forall>f\<in>(relations A). f a = 0"
   shows "\<forall>z::int \<noteq> 0. a [^] z \<noteq> \<one>"
 proof (rule ccontr; safe)
   fix z::int
   assume z: "z \<noteq> 0" "a [^] z = \<one>"
   have "restrict ((\<lambda>x. 0)(a := z)) A \<in> relations A"
     by (intro in_relationsI finprod_one_eqI, use z in auto)
   thus False using z assms by auto
 qed
 
 lemma (in comm_group) relations_zero_imp_ord_zero:
   assumes "a \<in> A" "\<forall>f\<in>(relations A). f a = 0"
   and "a \<in> carrier G"
   shows "ord a = 0"
   using assms relations_zero_imp_pow_not_one[OF assms(1, 2)]
   by (meson finite_cyclic_subgroup_int infinite_cyclic_subgroup_order)
 
 lemma (in comm_group) finprod_relations_triv_harder_better_stronger:
   assumes "A \<subseteq> carrier G" "relations A = {(\<lambda>_\<in>A. 0::int)}"
   shows "\<forall>f \<in> Pi\<^sub>E A (\<lambda>a. generate G {a}). finprod G f A = \<one> \<longrightarrow> (\<forall>a\<in>A. f a = \<one>)"
 proof(rule, rule)
   fix f
   assume f: "f \<in> (\<Pi>\<^sub>E a\<in>A. generate G {a})" "finprod G f A = \<one>"
-  with generate_pow assms(1) have "\<forall>a\<in>A. \<exists>k::int. f a = a [^] k" by auto
+  with generate_pow assms(1) have "\<forall>a\<in>A. \<exists>k::int. f a = a [^] k" by blast
   then obtain r::"'a \<Rightarrow> int" where r: "\<forall>a\<in>A. f a = a [^] r a" by metis
   have "restrict r A \<in> relations A"
   proof(intro in_relationsI)
     have "(\<Otimes>a\<in>A. a [^] restrict r A a) = finprod G f A"
       by (intro finprod_cong, use assms r in auto)
     thus "(\<Otimes>a\<in>A. a [^] restrict r A a) = \<one>" using f by simp
   qed simp
   with assms(2) have z: "restrict r A = (\<lambda>_\<in>A. 0)" by blast
   have "(restrict r A) a = r a" if "a \<in> A" for a using that by auto
   with r z show "\<forall>a\<in>A. f a = \<one>" by auto
 qed
 
 lemma (in comm_group) stronger_PiE_finprod_imp:
   assumes "A \<subseteq> carrier G" "\<forall>f \<in> Pi\<^sub>E A (\<lambda>a. generate G {a}). finprod G f A = \<one> \<longrightarrow> (\<forall>a\<in>A. f a = \<one>)"
   shows "\<forall>f \<in> Pi\<^sub>E ((\<lambda>a. generate G {a}) ` A) id.
          finprod G f ((\<lambda>a. generate G {a}) ` A) = \<one> \<longrightarrow> (\<forall>H\<in> (\<lambda>a. generate G {a}) ` A. f H = \<one>)"
 proof(rule, rule)
   fix f
   assume f: "f \<in> Pi\<^sub>E ((\<lambda>a. generate G {a}) ` A) id" "finprod G f ((\<lambda>a. generate G {a}) ` A) = \<one>"
   define B where "B = inv_into A (\<lambda>a. generate G {a}) ` ((\<lambda>a. generate G {a}) ` A)"
   have Bs: "B \<subseteq> A"
   proof
     fix x
     assume x: "x \<in> B"
     then obtain C where C: "C \<in> ((\<lambda>a. generate G {a}) ` A)" "x = inv_into A (\<lambda>a. generate G {a}) C"
       unfolding B_def by blast
     then obtain c where c: "C = generate G {c}" "c \<in> A" by blast
     with C someI_ex[of "\<lambda>y. y \<in> A \<and> generate G {y} = C"] show "x \<in> A"
       unfolding inv_into_def by blast
   qed
   have sI: "(\<lambda>x. generate G {x}) ` B = (\<lambda>x. generate G {x}) ` A"
   proof
     show "(\<lambda>x. generate G {x}) ` B \<subseteq> (\<lambda>x. generate G {x}) ` A" using Bs by blast
     show "(\<lambda>x. generate G {x}) ` A \<subseteq> (\<lambda>x. generate G {x}) ` B"
     proof
       fix C
       assume C: "C \<in> (\<lambda>x. generate G {x}) ` A"
       then obtain x where x: "x = inv_into A (\<lambda>a. generate G {a}) C" unfolding B_def by blast
       then obtain c where c: "C = generate G {c}" "c \<in> A" using C by blast
       with C x someI_ex[of "\<lambda>y. y \<in> A \<and> generate G {y} = C"] have "generate G {x} = C"
         unfolding inv_into_def by blast
       with x C show "C \<in> (\<lambda>x. generate G {x}) ` B" unfolding B_def by blast
     qed
   qed
   have fBc: "f (generate G {b}) \<in> carrier G" if "b \<in> B" for b
   proof -
     have "f (generate G {b}) \<in> generate G {b}" using f(1)
       by (subst (asm) sI[symmetric], use that in fastforce)
     moreover have "generate G {b} \<subseteq> carrier G" using assms(1) that Bs generate_incl by blast
     ultimately show ?thesis by blast
   qed
   let ?r = "restrict (\<lambda>a. if a\<in>B then f (generate G {a}) else \<one>) A"
   have "?r \<in> Pi\<^sub>E A (\<lambda>a. generate G {a})"
   proof
     show "?r x = undefined" if "x \<notin> A" for x using that by simp
     show "?r x \<in> generate G {x}" if "x \<in> A" for x using that generate.one B_def f(1) by auto
   qed
   moreover have "finprod G ?r A = \<one>"
   proof (cases "finite A")
     case True
     have "A = B \<union> (A - B)" using Bs by auto
     then have "finprod G ?r A = finprod G ?r (B\<union>(A-B))" by auto
     moreover have "\<dots> = finprod G ?r B \<otimes> finprod G ?r (A - B)"
     proof(intro finprod_Un_disjoint)
       from True Bs finite_subset show "finite B" "finite (A - B)" "B \<inter> (A - B) = {}" by auto
       show "(\<lambda>a\<in>A. if a \<in> B then f (generate G {a}) else \<one>) \<in> A - B \<rightarrow> carrier G" using Bs by simp
       from fBc show "(\<lambda>a\<in>A. if a \<in> B then f (generate G {a}) else \<one>) \<in> B \<rightarrow> carrier G"
         using Bs by auto
     qed
     moreover have "finprod G ?r B = \<one>"
     proof -
       have "finprod G ?r B = finprod G (f \<circ> (\<lambda>a. generate G {a})) B"
       proof(intro finprod_cong')
         show "?r b = (f \<circ> (\<lambda>a. generate G {a})) b" if "b \<in> B" for b using that Bs by auto
         show "f \<circ> (\<lambda>a. generate G {a}) \<in> B \<rightarrow> carrier G" using fBc by simp
       qed simp
       also have "\<dots> = finprod G f ((\<lambda>a. generate G {a}) ` B)"
       proof(intro finprod_comp[symmetric])
         show "(f \<circ> (\<lambda>a. generate G {a})) ` B \<subseteq> carrier G" using fBc by auto
         show "inj_on (\<lambda>a. generate G {a}) B"
           by (intro inj_onI, unfold B_def, metis (no_types, lifting) f_inv_into_f inv_into_into)
       qed
       also have "\<dots> = finprod G f ((\<lambda>a. generate G {a}) ` A)" using sI by argo
       finally show ?thesis using f(2) by argo
     qed
     moreover have "finprod G ?r (A - B) = \<one>" by(intro finprod_one_eqI, simp)
     ultimately show ?thesis by fastforce
   next
     case False
     then show ?thesis unfolding finprod_def by simp
   qed
   ultimately have a: "\<forall>a\<in>A. ?r a = \<one>" using assms(2) by blast
   then have BA: "\<forall>a\<in>B\<inter>A. ?r a = \<one>" by blast
   from Bs sI have "\<forall>a\<in>A. (generate G {a}) \<in> ((\<lambda>x. generate G {x}) ` B)" by simp
   then have "\<forall>a\<in>A. \<exists>b\<in>B. f (generate G {a}) = f (generate G {b})" by force
   thus "\<forall>H\<in>(\<lambda>a. generate G {a}) ` A. f H = \<one>" using a BA Bs by fastforce
 qed
 
 lemma (in comm_group) finprod_relations_triv:
   assumes "A \<subseteq> carrier G" "relations A = {(\<lambda>_\<in>A. 0::int)}"
   shows "\<forall>f \<in> Pi\<^sub>E ((\<lambda>a. generate G {a}) ` A) id.
          finprod G f ((\<lambda>a. generate G {a}) ` A) = \<one> \<longrightarrow> (\<forall>H\<in> (\<lambda>a. generate G {a}) ` A. f H = \<one>)"
   using assms finprod_relations_triv_harder_better_stronger stronger_PiE_finprod_imp by presburger
 
 lemma (in comm_group) ord_zero_strong_imp_rel_triv:
   assumes "A \<subseteq> carrier G" "\<forall>a \<in> A. ord a = 0"
   and "\<forall>f \<in> Pi\<^sub>E A (\<lambda>a. generate G {a}). finprod G f A = \<one> \<longrightarrow> (\<forall>a\<in>A. f a = \<one>)"
   shows "relations A = {(\<lambda>_\<in>A. 0::int)}"
 proof -
   have "\<And>r. r \<in> relations A \<Longrightarrow> r = (\<lambda>_\<in>A. 0::int)"
   proof
     fix r x
     assume r: "r \<in> relations A"
     show "r x = (\<lambda>_\<in>A. 0::int) x"
     proof (cases "x \<in> A")
       case True
       let ?r = "restrict (\<lambda>a. a [^] r a) A"
       have rp: "?r \<in> Pi\<^sub>E A (\<lambda>a. generate G {a})"
       proof -
         have "?r \<in> extensional A" by blast
         moreover have "?r \<in> Pi A (\<lambda>a. generate G {a})"
         proof
           fix a
           assume a: "a \<in> A"
           then have sga: "subgroup (generate G {a}) G" using generate_is_subgroup assms(1) by auto
           show "a [^] r a \<in> generate G {a}"
             using generate.incl[of a "{a}" G] subgroup_int_pow_closed[OF sga] by simp
         qed
         ultimately show ?thesis unfolding PiE_def by blast
       qed
       have "finprod G ?r A = (\<Otimes>a\<in>A. a [^] r a)" by(intro finprod_cong, use assms(1) in auto)
       with r have "finprod G ?r A = \<one>" unfolding relations_def by simp
       with assms(3) rp have "\<forall>a\<in>A. ?r a = \<one>" by fast
       then have "\<forall>a\<in>A. a [^] r a = \<one>" by simp
       with assms(1, 2) True have "r x = 0"
         using finite_cyclic_subgroup_int infinite_cyclic_subgroup_order by blast
       thus ?thesis using True by simp
     next
       case False
       thus ?thesis using r unfolding relations_def extensional_def by simp
     qed
   qed
   thus ?thesis using triv_rel by blast
 qed
 
 lemma (in comm_group) compl_fam_iff_relations_triv:
   assumes "finite gs" "gs \<subseteq> carrier G" "\<forall>g\<in>gs. ord g = 0"
   shows "relations gs = {(\<lambda>_\<in>gs. 0::int)} \<longleftrightarrow> compl_fam (\<lambda>g. generate G {g}) gs"
   using triv_finprod_iff_compl_fam_PiE[of _ "\<lambda>g. generate G {g}", OF assms(1) generate_is_subgroup]
         ord_zero_strong_imp_rel_triv[OF assms(2, 3)]
         finprod_relations_triv_harder_better_stronger[OF assms(2)] assms by blast
 
 end
diff --git a/thys/Finitely_Generated_Abelian_Groups/Miscellaneous_Groups.thy b/thys/Finitely_Generated_Abelian_Groups/Miscellaneous_Groups.thy
--- a/thys/Finitely_Generated_Abelian_Groups/Miscellaneous_Groups.thy
+++ b/thys/Finitely_Generated_Abelian_Groups/Miscellaneous_Groups.thy
@@ -1,239 +1,239 @@
 (*
     File:     Miscellaneous_Groups.thy
     Author:   Joseph Thommes, TU München
 *)
 section \<open>Miscellaneous group facts\<close>
 
 theory Miscellaneous_Groups
   imports Set_Multiplication
 begin
 
 text \<open>As the name suggests, this section contains several smaller lemmas about groups.\<close>
 
 (* Manuel Eberl *)
 lemma (in subgroup) nat_pow_closed [simp,intro]: "a \<in> H \<Longrightarrow> pow G a (n::nat) \<in> H"
   by (induction n) (auto simp: nat_pow_def)
 
 (* Manuel Eberl *)
 lemma nat_pow_modify_carrier: "a [^]\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> b = a [^]\<^bsub>G\<^esub> (b::nat)"
   by (simp add: nat_pow_def)
 
 lemma (in group) subgroup_card_dvd_group_ord:
   assumes "subgroup H G"
   shows "card H dvd order G"
   using Coset.group.lagrange[of G H] assms group_axioms by (metis dvd_triv_right)
 
 lemma (in group) subgroup_card_eq_order:
   assumes "subgroup H G"
   shows "card H = order (G\<lparr>carrier := H\<rparr>)"
   unfolding order_def by simp
 
 lemma (in group) finite_subgroup_card_neq_0:
   assumes "subgroup H G" "finite H"
   shows "card H \<noteq> 0"
   using subgroup_nonempty assms by auto
 
 lemma (in group) subgroup_order_dvd_group_order:
   assumes "subgroup H G"
   shows "order (G\<lparr>carrier := H\<rparr>) dvd order G"
   by (metis subgroup_card_dvd_group_ord[of H] assms subgroup_card_eq_order)
 
 lemma (in group) sub_subgroup_dvd_card:
   assumes "subgroup H G" "subgroup J G" "J \<subseteq> H"
   shows "card J dvd card H"
   by (metis subgroup_incl[of J H] subgroup_card_eq_order[of H]
             group.subgroup_card_dvd_group_ord[of "(G\<lparr>carrier := H\<rparr>)" J] assms
             subgroup.subgroup_is_group[of H G] group_axioms)
 
 lemma (in group) inter_subgroup_dvd_card:
   assumes "subgroup H G" "subgroup J G"
   shows "card (H \<inter> J) dvd card H"
   using subgroups_Inter_pair[of H J] assms sub_subgroup_dvd_card[of H "H \<inter> J"] by blast
 
 lemma (in group) subgroups_card_coprime_inter_card_one:
   assumes "subgroup H G" "subgroup J G" "coprime (card H) (card J)"
   shows "card (H \<inter> J) = 1"
 proof -
   from assms inter_subgroup_dvd_card have "is_unit (card (H \<inter> J))" unfolding coprime_def
-    by (meson Int_lower2 sub_subgroup_dvd_card subgroup_Int)
+    by (metis assms(3) coprime_common_divisor inf_commute)
   then show ?thesis by simp
 qed
 
 lemma (in group) coset_neq_imp_empty_inter:
   assumes "subgroup H G" "a \<in> carrier G" "b \<in> carrier G"
   shows "H #> a \<noteq> H #> b \<Longrightarrow> (H #> a) \<inter> (H #> b) = {}"
   by (metis Int_emptyI assms repr_independence)
 
 lemma (in comm_group) subgroup_is_comm_group:
   assumes "subgroup H G"
   shows "comm_group (G\<lparr>carrier := H\<rparr>)" unfolding comm_group_def
 proof
   interpret H: subgroup H G by fact
   interpret H: submonoid H G using H.subgroup_is_submonoid .
   show "Group.group (G\<lparr>carrier := H\<rparr>)" by blast
   show "comm_monoid (G\<lparr>carrier := H\<rparr>)" using submonoid_is_comm_monoid H.submonoid_axioms by blast
 qed
 
 lemma (in group) pow_int_mod_ord:
   assumes [simp]:"a \<in> carrier G" "ord a \<noteq> 0"
   shows "a [^] (n::int) = a [^] (n mod ord a)"
 proof -
   obtain q r where d: "q = n div ord a" "r = n mod ord a" "n = q * ord a + r"
     using mod_div_decomp by blast
   hence "a [^] n = (a [^] int (ord a)) [^] q \<otimes> a [^] r"
     using assms(1) int_pow_mult int_pow_pow
     by (metis mult_of_nat_commute)
   also have "\<dots> = \<one> [^] q \<otimes> a [^] r"
     by (simp add: int_pow_int)
   also have "\<dots> = a [^] r" by simp
   finally show ?thesis using d(2) by blast
 qed
 
 lemma (in group) pow_nat_mod_ord:
   assumes [simp]:"a \<in> carrier G" "ord a \<noteq> 0"
   shows "a [^] (n::nat) = a [^] (n mod ord a)"
 proof -
   obtain q r where d: "q = n div ord a" "r = n mod ord a" "n = q * ord a + r"
     using mod_div_decomp by blast
   hence "a [^] n = (a [^] ord a) [^] q \<otimes> a [^] r"
     using assms(1) nat_pow_mult nat_pow_pow by presburger
   also have "\<dots> = \<one> [^] q \<otimes> a [^] r" by auto
   also have "\<dots> = a [^] r" by simp
   finally show ?thesis using d(2) by blast
 qed
 
 lemma (in group) ord_min:
   assumes "m \<ge> 1" "x \<in> carrier G" "x [^] m = \<one>"
   shows   "ord x \<le> m"
   using assms pow_eq_id by auto
 
 (* Manuel Eberl *)
 lemma (in group) bij_betw_mult_left[intro]:
   assumes [simp]: "x \<in> carrier G"
   shows "bij_betw (\<lambda>y. x \<otimes> y) (carrier G) (carrier G)"
   by (intro bij_betwI[where ?g = "\<lambda>y. inv x \<otimes> y"])
      (auto simp: m_assoc [symmetric])
 
 (* Manuel Eberl *)
 lemma (in subgroup) inv_in_iff:
   assumes "x \<in> carrier G" "group G"
   shows   "inv x \<in> H \<longleftrightarrow> x \<in> H"
 proof safe
   assume "inv x \<in> H"
   hence "inv (inv x) \<in> H" by blast
   also have "inv (inv x) = x"
     by (intro group.inv_inv) (use assms in auto)
   finally show "x \<in> H" .
 qed auto
 
 (* Manuel Eberl *)
 lemma (in subgroup) mult_in_cancel_left:
   assumes "y \<in> carrier G" "x \<in> H" "group G"
   shows   "x \<otimes> y \<in> H \<longleftrightarrow> y \<in> H"
 proof safe
   assume "x \<otimes> y \<in> H"
   hence "inv x \<otimes> (x \<otimes> y) \<in> H"
     using assms by blast
   also have "inv x \<otimes> (x \<otimes> y) = y"
     using assms by (simp add: \<open>x \<otimes> y \<in> H\<close> group.inv_solve_left')
   finally show "y \<in> H" .
 qed (use assms in auto)
 
 (* Manuel Eberl *)
 lemma (in subgroup) mult_in_cancel_right:
   assumes "x \<in> carrier G" "y \<in> H" "group G"
   shows   "x \<otimes> y \<in> H \<longleftrightarrow> x \<in> H"
 proof safe
   assume "x \<otimes> y \<in> H"
   hence "(x \<otimes> y) \<otimes> inv y \<in> H"
     using assms by blast
   also have "(x \<otimes> y) \<otimes> inv y = x"
     using assms by (simp add: \<open>x \<otimes> y \<in> H\<close> group.inv_solve_right')
   finally show "x \<in> H" .
 qed (use assms in auto)
 
 lemma (in group) (* Manuel Eberl *)
   assumes "x \<in> carrier G" and "x [^] n = \<one>" and "n > 0"
   shows   ord_le: "ord x \<le> n" and ord_pos: "ord x > 0"
 proof -
   have "ord x dvd n"
     using pow_eq_id[of x n] assms by auto
   thus "ord x \<le> n" "ord x > 0"
     using assms by (auto intro: dvd_imp_le)
 qed
 
 lemma (in group) ord_conv_Least: (* Manuel Eberl *)
   assumes "x \<in> carrier G" "\<exists>n::nat > 0. x [^] n = \<one>"
   shows   "ord x = (LEAST n::nat. 0 < n \<and> x [^] n = \<one>)"
 proof (rule antisym)
   show "ord x \<le> (LEAST n::nat. 0 < n \<and> x [^] n = \<one>)"
     using assms LeastI_ex[OF assms(2)] by (intro ord_le) auto
   show "ord x \<ge> (LEAST n::nat. 0 < n \<and> x [^] n = \<one>)"
     using assms by (intro Least_le) (auto intro: pow_ord_eq_1 ord_pos)
 qed
 
 lemma (in group) ord_conv_Gcd: (* Manuel Eberl *)
   assumes "x \<in> carrier G"
   shows   "ord x = Gcd {n. x [^] n = \<one>}"
   by (rule sym, rule Gcd_eqI) (use assms in \<open>auto simp: pow_eq_id\<close>)
 
 lemma (in group) subgroup_ord_eq:
   assumes "subgroup H G" "x \<in> H"
   shows "group.ord (G\<lparr>carrier := H\<rparr>) x = ord x"
   using nat_pow_consistent ord_def group.ord_def[of "(G\<lparr>carrier := H\<rparr>)" x]
         subgroup.subgroup_is_group[of H G] assms by simp
 
 lemma (in group) ord_FactGroup:
   assumes "subgroup P G" "group (G Mod P)"
   shows "order (G Mod P) * card P = order G"
   using lagrange[of P] FactGroup_def[of G P] assms order_def[of "(G Mod P)"] by fastforce
 
 lemma (in group) one_is_same:
   assumes "subgroup H G"
   shows "\<one>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> = \<one>"
   by simp
 
 lemma (in group) kernel_FactGroup:
   assumes "P \<lhd> G"
   shows "kernel G (G Mod P) (\<lambda>x. P #> x) = P"
 proof(rule equalityI; rule subsetI)
   fix x
   assume "x \<in> kernel G (G Mod P) ((#>) P)"
   then have "P #> x = \<one>\<^bsub>G Mod P\<^esub>" "x \<in> carrier G" unfolding kernel_def by simp+
   with coset_join1[of P x] show "x \<in> P" using assms unfolding normal_def by simp
 next
   fix x
   assume x:"x \<in> P"
   then have xc: "x \<in> carrier G" using assms subgroup.subset unfolding normal_def by fast
   from x have "P #> x = P" using assms
     by (simp add: normal_imp_subgroup subgroup.rcos_const) 
   thus "x \<in> kernel G (G Mod P) ((#>) P)" unfolding kernel_def using xc by simp
 qed
 
 lemma (in group) sub_subgroup_coprime:
   assumes "subgroup H G" "subgroup J G" "coprime (card H) (card J)"
   and "subgroup sH G" "subgroup sJ G" "sH \<subseteq> H" "sJ \<subseteq> J"
 shows "coprime (card sH) (card sJ)"
   using assms by (meson coprime_divisors sub_subgroup_dvd_card)
 
 lemma (in group) pow_eq_nat_mod:
   assumes "a \<in> carrier G" "a [^] n = a [^] m"
   shows "n mod (ord a) = m mod (ord a)"
 proof -
   from assms have "a [^] (n - m) = \<one>" using pow_eq_div2 by blast
   hence "ord a dvd n - m" using assms(1) pow_eq_id by blast
   thus ?thesis
     by (metis assms mod_eq_dvd_iff_nat nat_le_linear pow_eq_div2 pow_eq_id)
 qed
 
 lemma (in group) pow_eq_int_mod:
   fixes n m::int
   assumes "a \<in> carrier G" "a [^] n = a [^] m"
   shows "n mod (ord a) = m mod (ord a)"
 proof -
   from assms have "a [^] (n - m) = \<one>" using int_pow_closed int_pow_diff r_inv by presburger
   hence "ord a dvd n - m" using assms(1) int_pow_eq_id by blast
   thus ?thesis by (meson mod_eq_dvd_iff)
 qed
 
 end
\ No newline at end of file
diff --git a/thys/Finitely_Generated_Abelian_Groups/Set_Multiplication.thy b/thys/Finitely_Generated_Abelian_Groups/Set_Multiplication.thy
--- a/thys/Finitely_Generated_Abelian_Groups/Set_Multiplication.thy
+++ b/thys/Finitely_Generated_Abelian_Groups/Set_Multiplication.thy
@@ -1,203 +1,203 @@
 (*
     File:     Set_Multiplication.thy
     Author:   Joseph Thommes, TU München
 *)
 section \<open>Set Multiplication\<close>
 
 theory Set_Multiplication
-  imports "HOL-Algebra.Algebra"
+  imports "HOL-Algebra.Multiplicative_Group"
 begin
 
 text \<open>This theory/section is of auxiliary nature and is mainly used to establish a connection
 between the set multiplication and the multiplication of subgroups via the \<open>IDirProd\<close> (although this
 particular notion is introduced later). However, as in every section of this entry, there are some
 lemmas that do not have any further usage in this entry, but are of interest just by themselves.\<close>
 
 lemma (in group) set_mult_union:
   "A <#> (B \<union> C) = (A <#> B) \<union> (A <#> C)"
   unfolding set_mult_def by auto
 
 lemma (in group) set_mult_card_single_el_eq:
   assumes "J \<subseteq> carrier G" "x \<in> carrier G"
   shows "card (l_coset G x J) = card J" unfolding l_coset_def
 proof -
   have "card ((\<otimes>) x ` J) = card J"
     using inj_on_cmult[of x] card_image[of "(\<otimes>) x" J] assms inj_on_subset[of "(\<otimes>) x" "carrier G" J]
     by blast
   moreover have "(\<Union>y\<in>J. {x \<otimes> y}) = (\<otimes>) x ` J" using image_def[of "(\<otimes>) x" J] by blast
   ultimately show "card (\<Union>h\<in>J. {x \<otimes> h}) = card J" by presburger
 qed
 
 text \<open>We find an upper bound for the cardinality of a set product.\<close>
 
 lemma (in group) set_mult_card_le:
   assumes "finite H" "H \<subseteq> carrier G" "J \<subseteq> carrier G"
   shows "card (H <#> J) \<le> card H * card J"
   using assms
 proof (induction "card H" arbitrary: H)
   case 0
   then have "H = {}" by force
   then show ?case using set_mult_def[of G H J] by simp
 next
   case (Suc n)
   then obtain a where a_def: "a \<in> H" by fastforce
   then have c_n: "card (H - {a}) = n" using Suc by force
   then have "card ((H - {a}) <#> J) \<le> card (H - {a}) * card J" using Suc by blast
   moreover have "card ({a} <#> J) = card J"
     using Suc(4, 5) a_def set_mult_card_single_el_eq[of J a] l_coset_eq_set_mult[of G a J] by auto
   moreover have "H <#> J = (H - {a} <#> J) \<union> ({a} <#> J)" using set_mult_def[of G _ J] a_def by auto
   moreover have "card (H - {a}) * card J + card J = Suc n * card J" using c_n mult_Suc by presburger
   ultimately show ?case using card_Un_le[of "H - {a} <#> J" "{a} <#> J"] c_n \<open>Suc n = card H\<close> by auto
 qed
 
 lemma (in group) set_mult_finite:
   assumes "finite H" "finite J" "H \<subseteq> carrier G" "J \<subseteq> carrier G"
   shows "finite (H <#> J)"
   using assms set_mult_def[of G H J] by auto
 
 text \<open>The next lemma allows us to later to derive that two finite subgroups $J$ and $H$ are complementary
 if and only if their product has the cardinality $|J| \cdot |H|$.\<close>
 
 lemma (in group) set_mult_card_eq_impl_empty_inter:
   assumes "finite H" "finite J" "H \<subseteq> carrier G" "J \<subseteq> carrier G" "card (H <#> J) = card H * card J"
   shows "\<And>a b. \<lbrakk>a \<in> H; b \<in> H; a \<noteq> b\<rbrakk> \<Longrightarrow> ((\<otimes>) a ` J) \<inter> ((\<otimes>) b ` J) = {}"
   using assms
 proof (induction H rule: finite_induct)
   case empty
   then show ?case by fast
 next
   case step: (insert x H)
   from step have x_c: "x \<in> carrier G" by simp
   from step have H_c: "H \<subseteq> carrier G" by simp
   from set_mult_card_single_el_eq[of J x] have card_x: "card ({x} <#> J) = card J"
     using \<open>J \<subseteq> carrier G\<close> x_c l_coset_eq_set_mult by metis
   moreover have ins: "(insert x H) <#> J = (H <#> J) \<union> ({x} <#> J)"
     using set_mult_def[of G _ J] by auto
   ultimately have "card (H <#> J) \<ge> card H * card J"
     using card_Un_le[of "H <#> J" "{x} <#> J"] \<open>card (insert x H <#> J) = card (insert x H) * card J\<close>
     by (simp add: step.hyps(1) step.hyps(2))
   then have card_eq:"card (H <#> J) = card H * card J"
     using set_mult_card_le[of H J] step H_c by linarith
   then have ih: "\<And>a b. \<lbrakk>a \<in> H; b \<in> H; a \<noteq> b\<rbrakk> \<Longrightarrow> ((\<otimes>) a ` J) \<inter> ((\<otimes>) b ` J) = {}"
     using step H_c by presburger
 
   have "card (insert x H) * card J = card H * card J + card J" using \<open>x \<notin> H\<close> using step by simp
   then have "({x} <#> J) \<inter> (H <#> J) = {}"
     using card_eq card_x ins card_Un_Int[of "H <#> J" "{x} <#> J"] step set_mult_finite by auto
   then have "\<And>a. a \<in> H \<Longrightarrow> (\<Union>y\<in>J. {a \<otimes> y}) \<inter> (\<Union>y\<in>J. {x \<otimes> y}) = {}" 
     using set_mult_def[of G _ J] by blast
   then have "\<And>a b. \<lbrakk>a \<in> (insert x H); b \<in> (insert x H); a \<noteq> b\<rbrakk> \<Longrightarrow> ((\<otimes>) a ` J) \<inter> ((\<otimes>) b ` J) = {}"
     using \<open>x \<notin> H\<close> ih by blast
-  then show ?case using step by algebra
+  then show ?case using step by presburger
 qed
 
 lemma (in group) set_mult_card_eq_impl_empty_inter':
   assumes "finite H" "finite J" "H \<subseteq> carrier G" "J \<subseteq> carrier G" "card (H <#> J) = card H * card J"
   shows "\<And>a b. \<lbrakk>a \<in> H; b \<in> H; a \<noteq> b\<rbrakk> \<Longrightarrow> (l_coset G a J) \<inter> (l_coset G b J) = {}"
   unfolding l_coset_def
   using set_mult_card_eq_impl_empty_inter image_def[of "(\<otimes>) _" J] assms by blast
 
 lemma (in comm_group) set_mult_comm:
   assumes "H \<subseteq> carrier G" "J \<subseteq> carrier G"
   shows "(H <#> J) = (J <#> H)"
   unfolding set_mult_def
 proof -
   have 1: "\<And>a b. \<lbrakk>a \<in> carrier G; b \<in> carrier G\<rbrakk> \<Longrightarrow> {a \<otimes> b} = {b \<otimes> a}" using m_comm by simp
   then have "\<And>a b.\<lbrakk>a \<in> H; b \<in> J\<rbrakk> \<Longrightarrow> {a \<otimes> b} = {b \<otimes> a}" using assms by auto
   moreover have "\<And>a b.\<lbrakk>b \<in> H; a \<in> J\<rbrakk> \<Longrightarrow> {a \<otimes> b} = {b \<otimes> a}" using assms 1 by auto
   ultimately show "(\<Union>h\<in>H. \<Union>k\<in>J. {h \<otimes> k}) = (\<Union>k\<in>J. \<Union>h\<in>H. {k \<otimes> h})"  by fast
 qed
 
 lemma (in group) set_mult_one_imp_inc:
   assumes "\<one> \<in> A" "A \<subseteq> carrier G" "B \<subseteq> carrier G"
   shows "B \<subseteq> (B <#> A)"
 proof
   fix x
   assume "x \<in> B"
   thus "x \<in> (B <#> A)" using assms unfolding set_mult_def by force
 qed
 
 text \<open>In all cases, we know that the product of two sets is always contained in the subgroup
 generated by them.\<close>
 lemma (in group) set_mult_subset_generate:
   assumes "A \<subseteq> carrier G" "B \<subseteq> carrier G"
   shows "A <#> B \<subseteq> generate G (A \<union> B)"
 proof
   fix x
   assume "x \<in> A <#> B"
   then obtain a b where ab: "a \<in> A" "b \<in> B" "x = a \<otimes> b" unfolding set_mult_def by blast
   then have "a \<in> generate G (A \<union> B)" "b \<in> generate G (A \<union> B)"
     using generate.incl[of _ "A \<union> B" G] by simp+
   thus "x \<in> generate G (A \<union> B)" using ab generate.eng by metis
 qed
 
 text \<open>In the case of subgroups, the set product is just the subgroup generated by both
 of the subgroups.\<close>
 
 lemma (in comm_group) set_mult_eq_generate_subgroup:
   assumes "subgroup H G" "subgroup J G"
   shows "generate G (H \<union> J) = H <#> J" (is "?L = ?R")
 proof
   show "?L \<subseteq> ?R"
   proof
     fix x
     assume "x \<in> ?L"
     then show "x \<in> ?R"
     proof(induction rule: generate.induct)
       case one
       have "\<one> \<otimes> \<one> = \<one>" using nat_pow_one[of 2] by simp
       thus ?case
         using assms subgroup.one_closed[OF assms(1)]
               subgroup.one_closed[OF assms(2)] set_mult_def[of G H J] by fastforce
     next
       case (incl x)
       have H1: "\<one> \<in> H" using assms subgroup.one_closed by auto
       have J1: "\<one> \<in> J" using assms subgroup.one_closed by auto
       have lx: "x \<otimes> \<one> = x" using r_one[of x] incl subgroup.subset assms by blast
       have rx: "\<one> \<otimes> x = x" using l_one[of x] incl subgroup.subset assms by blast
       show ?case
       proof (cases "x \<in> H")
         case True
         then show ?thesis using set_mult_def J1 lx by fastforce
       next
         case False
         then show ?thesis using set_mult_def H1 rx incl by fastforce
       qed
     next
       case (inv h)
       then have inv_in:"(inv h) \<in> H \<union> J" (is "?iv \<in> H \<union> J")
         using assms subgroup.m_inv_closed[of _ G h] by (cases "h \<in> H"; blast)
       have H1: "\<one> \<in> H" using assms subgroup.one_closed by auto
       have J1: "\<one> \<in> J" using assms subgroup.one_closed by auto
       have lx: "?iv \<otimes> \<one> = ?iv" using r_one[of "?iv"] subgroup.subset inv_in assms by blast
       have rx: "\<one> \<otimes> ?iv = ?iv" using l_one[of "?iv"] incl subgroup.subset inv_in assms by blast
       show ?case 
       proof (cases "?iv \<in> H")
         case True
         then show ?thesis using set_mult_def[of G H J] J1 lx by fastforce
       next
         case False
         then show ?thesis using set_mult_def[of G H J] H1 rx inv_in by fastforce
       qed
     next
       case (eng h g)
       from eng(3) obtain a b where aH: "a \<in> H" and bJ: "b \<in> J" and h_def: "h = a \<otimes> b"
         using set_mult_def[of G H J] by fast
       have a_carr: "a \<in> carrier G" by (metis subgroup.mem_carrier assms(1) aH)
       have b_carr: "b \<in> carrier G" by (metis subgroup.mem_carrier assms(2) bJ)
       from eng(4) obtain c d where cH: "c \<in> H" and dJ: "d \<in> J" and g_def: "g = c \<otimes> d"
         using set_mult_def[of G H J] by fast
       have c_carr: "c \<in> carrier G" by (metis subgroup.mem_carrier assms(1) cH)
       have d_carr: "d \<in> carrier G" by (metis subgroup.mem_carrier assms(2) dJ)
       then have "h \<otimes> g = (a \<otimes> c) \<otimes> (b \<otimes> d)"
         using a_carr b_carr c_carr d_carr g_def h_def m_assoc m_comm by force
       moreover have "a \<otimes> c \<in> H" using assms(1) aH cH subgroup.m_closed by fast
       moreover have "b \<otimes> d \<in> J" using assms(2) bJ dJ subgroup.m_closed by fast
       ultimately show ?case using set_mult_def by fast
     qed
   qed
 next
   show "?R \<subseteq> ?L" using set_mult_subset_generate[of H J] subgroup.subset assms by blast
 qed
 
 end
\ No newline at end of file