diff --git a/thys/Hermite_Lindemann/Algebraic_Integer_Divisibility.thy b/thys/Hermite_Lindemann/Algebraic_Integer_Divisibility.thy
new file mode 100644
--- /dev/null
+++ b/thys/Hermite_Lindemann/Algebraic_Integer_Divisibility.thy
@@ -0,0 +1,221 @@
+(*
+  File:     Algebraic_Integer_Divisibility.thy
+  Author:   Manuel Eberl, TU München
+*)
+section \<open>Divisibility of algebraic integers\<close>
+theory Algebraic_Integer_Divisibility
+  imports "Algebraic_Numbers.Algebraic_Numbers"
+begin
+
+text \<open>
+  In this section, we define a notion of divisibility of algebraic integers: \<open>y\<close> is divisible
+  by \<open>x\<close> if \<open>y / x\<close> is an algebraic integer (or if \<open>x\<close> and \<open>y\<close> are both zero).
+
+  Technically, the definition does not require \<open>x\<close> and \<open>y\<close> to be algebraic integers themselves,
+  but we will always use it that way (in fact, in our case \<open>x\<close> will always be a rational integer).
+\<close>
+
+definition alg_dvd :: "'a :: field \<Rightarrow> 'a \<Rightarrow> bool" (infix "alg'_dvd" 50) where
+  "x alg_dvd y \<longleftrightarrow> (x = 0 \<longrightarrow> y = 0) \<and> algebraic_int (y / x)"
+
+lemma alg_dvd_imp_algebraic_int:
+  fixes x y :: "'a :: field_char_0"
+  shows "x alg_dvd y \<Longrightarrow> algebraic_int x \<Longrightarrow> algebraic_int y"
+  using algebraic_int_times[of "y / x" x] by (auto simp: alg_dvd_def)
+
+lemma alg_dvd_0_left_iff [simp]: "0 alg_dvd x \<longleftrightarrow> x = 0"
+  by (auto simp: alg_dvd_def)
+
+lemma alg_dvd_0_right [iff]: "x alg_dvd 0"
+  by (auto simp: alg_dvd_def)
+
+lemma one_alg_dvd_iff [simp]: "1 alg_dvd x \<longleftrightarrow> algebraic_int x"
+  by (auto simp: alg_dvd_def)
+
+lemma alg_dvd_of_int [intro]:
+  assumes "x dvd y"
+  shows   "of_int x alg_dvd of_int y"
+proof (cases "of_int x = (0 :: 'a)")
+  case False
+  from assms obtain z where z: "y = x * z"
+    by (elim dvdE)
+  have "algebraic_int (of_int z)"
+    by auto
+  also have "of_int z = of_int y / (of_int x :: 'a)"
+    using False by (simp add: z field_simps)
+  finally show ?thesis
+    using False by (simp add: alg_dvd_def)
+qed (use assms in \<open>auto simp: alg_dvd_def\<close>)
+
+lemma alg_dvd_of_nat [intro]:
+  assumes "x dvd y"
+  shows   "of_nat x alg_dvd of_nat y"
+  using alg_dvd_of_int[of "int x" "int y"] assms by simp
+
+lemma alg_dvd_of_int_iff [simp]:
+  "(of_int x :: 'a :: field_char_0) alg_dvd of_int y \<longleftrightarrow> x dvd y"
+proof
+  assume "(of_int x :: 'a) alg_dvd of_int y"
+  hence "of_int y / (of_int x :: 'a) \<in> \<int>" and nz: "of_int x = (0::'a) \<longrightarrow> of_int y = (0::'a)"
+    by (auto simp: alg_dvd_def dest!: rational_algebraic_int_is_int)
+  then obtain n where "of_int y / of_int x = (of_int n :: 'a)"
+    by (elim Ints_cases)
+  hence "of_int y = (of_int (x * n) :: 'a)"
+    unfolding of_int_mult using nz by (auto simp: field_simps)
+  hence "y = x * n"
+    by (subst (asm) of_int_eq_iff)
+  thus "x dvd y"
+    by auto
+qed blast
+
+lemma alg_dvd_of_nat_iff [simp]:
+  "(of_nat x :: 'a :: field_char_0) alg_dvd of_nat y \<longleftrightarrow> x dvd y"
+proof -
+  have "(of_int (int x) :: 'a) alg_dvd of_int (int y) \<longleftrightarrow> x dvd y"
+    by (subst alg_dvd_of_int_iff) auto
+  thus ?thesis unfolding of_int_of_nat_eq .
+qed
+
+lemma alg_dvd_add [intro]:
+  fixes x y z :: "'a :: field_char_0"
+  shows "x alg_dvd y \<Longrightarrow> x alg_dvd z \<Longrightarrow> x alg_dvd (y + z)"
+  unfolding alg_dvd_def by (auto simp: add_divide_distrib)
+
+lemma alg_dvd_uminus_right [intro]: "x alg_dvd y \<Longrightarrow> x alg_dvd -y"
+  by (auto simp: alg_dvd_def)
+
+lemma alg_dvd_uminus_right_iff [simp]: "x alg_dvd -y \<longleftrightarrow> x alg_dvd y"
+  using alg_dvd_uminus_right[of x y] alg_dvd_uminus_right[of x "-y"] by auto
+
+lemma alg_dvd_diff [intro]:
+  fixes x y z :: "'a :: field_char_0"
+  shows "x alg_dvd y \<Longrightarrow> x alg_dvd z \<Longrightarrow> x alg_dvd (y - z)"
+  unfolding alg_dvd_def by (auto simp: diff_divide_distrib)
+
+lemma alg_dvd_triv_left [intro]: "algebraic_int y \<Longrightarrow> x alg_dvd x * y"
+  by (auto simp: alg_dvd_def)
+
+lemma alg_dvd_triv_right [intro]: "algebraic_int x \<Longrightarrow> y alg_dvd x * y"
+  by (auto simp: alg_dvd_def)
+
+lemma alg_dvd_triv_left_iff: "x alg_dvd x * y \<longleftrightarrow> x = 0 \<or> algebraic_int y"
+  by (auto simp: alg_dvd_def)
+
+lemma alg_dvd_triv_right_iff: "y alg_dvd x * y \<longleftrightarrow> y = 0 \<or> algebraic_int x"
+  by (auto simp: alg_dvd_def)
+
+lemma alg_dvd_triv_left_iff' [simp]: "x \<noteq> 0 \<Longrightarrow> x alg_dvd x * y \<longleftrightarrow> algebraic_int y"
+  by (simp add: alg_dvd_triv_left_iff)
+
+lemma alg_dvd_triv_right_iff' [simp]: "y \<noteq> 0 \<Longrightarrow> y alg_dvd x * y \<longleftrightarrow> algebraic_int x"
+  by (simp add: alg_dvd_triv_right_iff)
+
+lemma alg_dvd_trans [trans]:
+  fixes x y z :: "'a :: field_char_0"
+  shows "x alg_dvd y \<Longrightarrow> y alg_dvd z \<Longrightarrow> x alg_dvd z"
+  using algebraic_int_times[of "y / x" "z / y"] by (auto simp: alg_dvd_def)
+
+lemma alg_dvd_mono [simp]: 
+  fixes a b c d :: "'a :: field_char_0"
+  shows "a alg_dvd c \<Longrightarrow> b alg_dvd d \<Longrightarrow> (a * b) alg_dvd (c * d)"
+  using algebraic_int_times[of "c / a" "d / b"] by (auto simp: alg_dvd_def)
+
+lemma alg_dvd_mult [simp]: 
+  fixes a b c :: "'a :: field_char_0"
+  shows "a alg_dvd c \<Longrightarrow> algebraic_int b \<Longrightarrow> a alg_dvd (b * c)"
+  using alg_dvd_mono[of a c 1 b] by (auto simp: mult.commute)
+
+lemma alg_dvd_mult2 [simp]:
+  fixes a b c :: "'a :: field_char_0"
+  shows "a alg_dvd b \<Longrightarrow> algebraic_int c \<Longrightarrow> a alg_dvd (b * c)"
+  using alg_dvd_mult[of a b c] by (simp add: mult.commute)
+
+text \<open>
+  A crucial theorem: if an integer \<open>x\<close> divides a rational number \<open>y\<close>, then \<open>y\<close> is in fact
+  also an integer, and that integer is a multiple of \<open>x\<close>.
+\<close>
+lemma alg_dvd_int_rat:
+  fixes y :: "'a :: field_char_0"
+  assumes "of_int x alg_dvd y" and "y \<in> \<rat>"
+  shows   "\<exists>n. y = of_int n \<and> x dvd n"
+proof (cases "x = 0")
+  case False
+  have "y / of_int x \<in> \<int>"
+    by (intro rational_algebraic_int_is_int) (use assms in \<open>auto simp: alg_dvd_def\<close>)
+  then obtain n where n: "of_int n = y / (of_int x :: 'a)"
+    by (elim Ints_cases) auto
+  hence "y = of_int (n * x)"
+    using False by (simp add: field_simps)
+  thus ?thesis by (intro exI[of _ "x * n"]) auto
+qed (use assms in auto)
+
+lemma prod_alg_dvd_prod:
+  fixes f :: "'a \<Rightarrow> 'b :: field_char_0"
+  assumes "\<And>x. x \<in> A \<Longrightarrow> f x alg_dvd g x"
+  shows   "prod f A alg_dvd prod g A"
+  using assms by (induction A rule: infinite_finite_induct) auto
+
+lemma alg_dvd_sum:
+  fixes f :: "'a \<Rightarrow> 'b :: field_char_0"
+  assumes "\<And>x. x \<in> A \<Longrightarrow> y alg_dvd f x"
+  shows   "y alg_dvd sum f A"
+  using assms by (induction A rule: infinite_finite_induct) auto
+
+lemma not_alg_dvd_sum:
+  fixes f :: "'a \<Rightarrow> 'b :: field_char_0"
+  assumes "\<And>x. x \<in> A-{x'} \<Longrightarrow> y alg_dvd f x"
+  assumes "\<not>y alg_dvd f x'"
+  assumes "x' \<in> A" "finite A"
+  shows   "\<not>y alg_dvd sum f A"
+proof
+  assume *: "y alg_dvd sum f A"
+  have "y alg_dvd sum f A - sum f (A - {x'})"
+    using \<open>x' \<in> A\<close> by (intro alg_dvd_diff[OF * alg_dvd_sum] assms) auto
+  also have "\<dots> = sum f (A - (A - {x'}))"
+    using assms by (subst sum_diff) auto
+  also have "A - (A - {x'}) = {x'}"
+    using assms by auto
+  finally show False using assms by simp
+qed
+
+lemma fact_dvd_pochhammer:
+  assumes "m \<le> n + 1"
+  shows   "fact m dvd pochhammer (int n - int m + 1) m"
+proof -
+  have "(real n gchoose m) * fact m = of_int (pochhammer (int n - int m + 1) m)"
+    by (simp add: gbinomial_pochhammer' pochhammer_of_int [symmetric])
+  also have "(real n gchoose m) * fact m = of_int (int (n choose m) * fact m)"
+    by (simp add: binomial_gbinomial)
+  finally have "int (n choose m) * fact m = pochhammer (int n - int m + 1) m"
+    by (subst (asm) of_int_eq_iff)
+  from this [symmetric] show ?thesis by simp
+qed
+
+lemma coeff_higher_pderiv:
+  "coeff ((pderiv ^^ m) f) n = pochhammer (of_nat (Suc n)) m * coeff f (n + m)"
+  by (induction m arbitrary: n) (simp_all add: coeff_pderiv pochhammer_rec algebra_simps)
+
+lemma fact_alg_dvd_poly_higher_pderiv:
+  fixes p :: "'a :: field_char_0 poly"
+  assumes "\<And>i. algebraic_int (poly.coeff p i)" "algebraic_int x" "m \<le> k"
+  shows   "fact m alg_dvd poly ((pderiv ^^ k) p) x"
+  unfolding poly_altdef
+proof (intro alg_dvd_sum, goal_cases)
+  case (1 i)
+  have "(of_int (fact m) :: 'a) alg_dvd (of_int (fact k))"
+    by (intro alg_dvd_of_int fact_dvd assms)
+  also have "(of_int (fact k) :: 'a) alg_dvd of_int (pochhammer (int i + 1) k)"
+    using fact_dvd_pochhammer[of k "i + k"]
+    by (intro alg_dvd_of_int fact_dvd_pochhammer) (auto simp: algebra_simps)
+  finally have "fact m alg_dvd (pochhammer (of_nat i + 1) k :: 'a)"
+    by (simp flip: pochhammer_of_int)
+  also have "\<dots> alg_dvd pochhammer (of_nat i + 1) k * poly.coeff p (i + k)"
+    by (rule alg_dvd_triv_left) (rule assms)
+  also have "\<dots> = poly.coeff ((pderiv ^^ k) p) i"
+    unfolding coeff_higher_pderiv by (simp add: add_ac flip: pochhammer_of_int)
+  also have "\<dots> alg_dvd poly.coeff ((pderiv ^^ k) p) i * x ^ i"
+    by (intro alg_dvd_triv_left algebraic_int_power assms)
+  finally show ?case .
+qed
+
+end
\ No newline at end of file
diff --git a/thys/Hermite_Lindemann/Complex_Lexorder.thy b/thys/Hermite_Lindemann/Complex_Lexorder.thy
new file mode 100644
--- /dev/null
+++ b/thys/Hermite_Lindemann/Complex_Lexorder.thy
@@ -0,0 +1,89 @@
+(*
+  File:     Complex_Lexorder.thy
+  Author:   Manuel Eberl, TU München
+*)
+section \<open>The lexicographic ordering on complex numbers\<close>
+theory Complex_Lexorder
+  imports Complex_Main "HOL-Library.Multiset"
+begin
+
+text \<open>
+  We define a lexicographic order on the complex numbers, comparing first the real parts
+  and, if they are equal, the imaginary parts. This ordering is of course not compatible with
+  multiplication, but it is compatible with addition.
+\<close>
+
+definition less_eq_complex_lex (infix "\<le>\<^sub>\<complex>" 50)  where
+  "less_eq_complex_lex x y \<longleftrightarrow> Re x < Re y \<or> Re x = Re y \<and> Im x \<le> Im y"
+
+definition less_complex_lex (infix "<\<^sub>\<complex>" 50) where
+  "less_complex_lex x y \<longleftrightarrow> Re x < Re y \<or> Re x = Re y \<and> Im x < Im y"
+
+interpretation complex_lex:
+  linordered_ab_group_add "(+)" 0 "(-)" "uminus" less_eq_complex_lex less_complex_lex
+  by standard (auto simp: less_eq_complex_lex_def less_complex_lex_def complex_eq_iff)
+
+lemmas [trans] =
+  complex_lex.order.trans complex_lex.less_le_trans
+  complex_lex.less_trans complex_lex.le_less_trans
+
+lemma (in ordered_comm_monoid_add) sum_mono_complex_lex:
+  "(\<And>i. i\<in>K \<Longrightarrow> f i \<le>\<^sub>\<complex> g i) \<Longrightarrow> (\<Sum>i\<in>K. f i) \<le>\<^sub>\<complex> (\<Sum>i\<in>K. g i)"
+  by (induct K rule: infinite_finite_induct) (use complex_lex.add_mono in auto)
+
+lemma sum_strict_mono_ex1_complex_lex:
+  fixes f g :: "'i \<Rightarrow> complex"
+  assumes "finite A"
+    and "\<forall>x\<in>A. f x \<le>\<^sub>\<complex> g x"
+    and "\<exists>a\<in>A. f a <\<^sub>\<complex> g a"
+  shows "sum f A <\<^sub>\<complex> sum g A"
+proof-
+  from assms(3) obtain a where a: "a \<in> A" "f a <\<^sub>\<complex> g a" by blast
+  have "sum f A = sum f ((A - {a}) \<union> {a})"
+    by (simp add: insert_absorb[OF \<open>a \<in> A\<close>])
+  also have "\<dots> = sum f (A - {a}) + sum f {a}"
+    using \<open>finite A\<close> by (subst sum.union_disjoint) auto
+  also have "\<dots> \<le>\<^sub>\<complex> sum g (A - {a}) + sum f {a}"
+    by (intro complex_lex.add_mono sum_mono_complex_lex) (simp_all add: assms)
+  also have "\<dots> <\<^sub>\<complex> sum g (A - {a}) + sum g {a}"
+    using a by (intro complex_lex.add_strict_left_mono) auto
+  also have "\<dots> = sum g ((A - {a}) \<union> {a})"
+    using \<open>finite A\<close> by (subst sum.union_disjoint[symmetric]) auto
+  also have "\<dots> = sum g A" by (simp add: insert_absorb[OF \<open>a \<in> A\<close>])
+  finally show ?thesis
+    by simp
+qed
+
+lemma sum_list_mono_complex_lex:
+  assumes "list_all2 (\<le>\<^sub>\<complex>) xs ys"
+  shows   "sum_list xs \<le>\<^sub>\<complex> sum_list ys"
+  using assms by induction (auto intro: complex_lex.add_mono)
+
+lemma sum_mset_mono_complex_lex:
+  assumes "rel_mset (\<le>\<^sub>\<complex>) A B"
+  shows   "sum_mset A \<le>\<^sub>\<complex> sum_mset B"
+  using assms by (auto simp: rel_mset_def sum_mset_sum_list intro: sum_list_mono_complex_lex)
+
+lemma rel_msetI:
+  assumes "list_all2 R xs ys" "mset xs = A" "mset ys = B"
+  shows   "rel_mset R A B"
+  using assms by (auto simp: rel_mset_def)
+
+lemma mset_replicate [simp]: "mset (replicate n x) = replicate_mset n x"
+  by (induction n) auto
+
+lemma rel_mset_replicate_mset_right:
+  assumes "\<And>x. x \<in># A \<Longrightarrow> R x y" "size A = n"
+  shows   "rel_mset R A (replicate_mset n y)"
+proof -
+  obtain xs where [simp]: "A = mset xs"
+    by (metis ex_mset)
+  from assms have "\<forall>x\<in>set xs. R x y"
+    by auto
+  hence "list_all2 R xs (replicate (length xs) y)"
+    by (induction xs) auto
+  with assms(2) show ?thesis
+    by (intro rel_msetI[of R xs "replicate n y"]) auto
+qed
+
+end
\ No newline at end of file
diff --git a/thys/Hermite_Lindemann/Hermite_Lindemann.thy b/thys/Hermite_Lindemann/Hermite_Lindemann.thy
new file mode 100644
--- /dev/null
+++ b/thys/Hermite_Lindemann/Hermite_Lindemann.thy
@@ -0,0 +1,2558 @@
+(*
+  File:     Hermite_Lindemann.thy
+  Author:   Manuel Eberl, TU München
+*)
+section \<open>The Hermite--Lindemann--Weierstraß Transcendence Theorem\<close>
+theory Hermite_Lindemann
+imports 
+  Pi_Transcendental.Pi_Transcendental
+  Algebraic_Numbers.Algebraic_Numbers
+  Algebraic_Integer_Divisibility
+  Min_Int_Poly
+  Complex_Lexorder
+  More_Polynomial_HLW
+  More_Multivariate_Polynomial_HLW
+  More_Algebraic_Numbers_HLW
+  Misc_HLW
+begin
+
+text \<open>
+  The Hermite--Lindemann--Weierstraß theorem answers questions about the transcendence of
+  the exponential function and other related complex functions. It proves that a large number of
+  combinations of exponentials is always transcendental.
+
+  A first (much weaker) version of the theorem was proven by Hermite. Lindemann and Weierstraß then
+  successively generalised it shortly afterwards, and finally Baker gave another, arguably more
+  elegant formulation (which is the one that we will prove, and then derive the traditional version
+  from it).
+
+  To honour the contributions of all three of these 19th-century mathematicians, I refer to the
+  theorem as the Hermite--Lindemann--Weierstraß theorem, even though in other literature it is
+  often called Hermite--Lindemann or Lindemann--Weierstraß. To keep things short, the Isabelle
+  name of the theorem, however, will omit Weierstraß's name.
+\<close>
+
+subsection \<open>Main proof\<close>
+
+text \<open>
+  Following Baker, We first prove the following special form of the theorem:
+  Let $m > 0$ and $q_1, \ldots, q_m \in\mathbb{Z}[X]$ be irreducible, non-constant,
+  and pairwise coprime polynomials. Let $\beta_1, \ldots, \beta_m$ be non-zero integers. Then
+  \[\sum_{i=1}^m \beta_i \sum_{q_i(\alpha) = 0} e^\alpha \neq 0\]
+
+  The difference to the final theorem is that
+
+    \<^enum> The coefficients $\beta_i$ are non-zero integers (as opposed to arbitrary algebraic numbers)
+
+    \<^enum> The exponents $\alpha_i$ occur in full sets of conjugates, and each set has the same
+      coefficient.
+
+  In a similar fashion to the proofs of the transcendence of \<open>e\<close> and \<open>\<pi>\<close>, we define some number
+  $J$ depending on the $\alpha_i$ and $\beta_i$ and an arbitrary sufficiently large prime \<open>p\<close>. We
+  then show that, on one hand, $J$ is an integer multiple of $(p-1)!$, but on the other hand it
+  is bounded from above by a term of the form $C_1 \cdot C_2^p$. This is then clearly a
+  contradiction if \<open>p\<close> is chosen large enough.
+\<close>
+
+lemma Hermite_Lindemann_aux1:
+  fixes P :: "int poly set" and \<beta> :: "int poly \<Rightarrow> int"
+  assumes "finite P" and "P \<noteq> {}"
+  assumes distinct: "pairwise Rings.coprime P"
+  assumes irred: "\<And>p. p \<in> P \<Longrightarrow> irreducible p"
+  assumes nonconstant: "\<And>p. p \<in> P \<Longrightarrow> Polynomial.degree p > 0"
+  assumes \<beta>_nz: "\<And>p. p \<in> P \<Longrightarrow> \<beta> p \<noteq> 0"
+  defines "Roots \<equiv> (\<lambda>p. {\<alpha>::complex. poly (of_int_poly p) \<alpha> = 0})"
+  shows   "(\<Sum>p\<in>P. of_int (\<beta> p) * (\<Sum>\<alpha>\<in>Roots p. exp \<alpha>)) \<noteq> 0"
+proof
+  note [intro] = \<open>finite P\<close>
+  assume sum_eq_0: "(\<Sum>p\<in>P. of_int (\<beta> p) * (\<Sum>\<alpha>\<in>Roots p. exp \<alpha>)) = 0"
+
+  define Roots' where "Roots' = (\<Union>p\<in>P. Roots p)"
+  have finite_Roots [intro]: "finite (Roots p)" if "p \<in> P" for p
+    using nonconstant[of p] that by (auto intro: poly_roots_finite simp: Roots_def)
+  have [intro]: "finite Roots'"
+    by (auto simp: Roots'_def)
+  have [simp]: "0 \<notin> P"
+    using nonconstant[of 0] by auto
+  have [simp]: "p \<noteq> 0" if "p \<in> P" for p
+    using that by auto
+
+  text \<open>
+    The polynomials in \<^term>\<open>P\<close> do not have multiple roots:
+  \<close>
+  have rsquarefree: "rsquarefree (of_int_poly q :: complex poly)" if "q \<in> P" for q
+    by (rule irreducible_imp_rsquarefree_of_int_poly) (use that in \<open>auto intro: irred nonconstant\<close>)
+
+  text \<open>
+    No two different polynomials in \<^term>\<open>P\<close> have roots in common:
+  \<close>
+  have disjoint: "disjoint_family_on Roots P"
+    using distinct
+  proof (rule pairwise_imp_disjoint_family_on)
+    fix p q assume P: "p \<in> P" "q \<in> P" and "Rings.coprime p q"
+    hence "Rings.coprime (of_int_poly p :: complex poly) (of_int_poly q)"
+      by (intro coprime_of_int_polyI)
+    thus "Roots p \<inter> Roots q = {}"
+      using poly_eq_0_coprime[of "of_int_poly p" "of_int_poly q :: complex poly"] P
+      by (auto simp: Roots_def)
+  qed
+
+  define n_roots :: "int poly \<Rightarrow> nat" ("\<sharp>_")
+    where "n_roots = (\<lambda>p. card (Roots p))"
+  define n where "n = (\<Sum>p\<in>P. \<sharp>p)"
+  have n_altdef: "n = card Roots'"
+    unfolding n_def Roots'_def n_roots_def using disjoint
+    by (subst card_UN_disjoint) (auto simp: disjoint_family_on_def)
+  have Roots_nonempty: "Roots p \<noteq> {}" if "p \<in> P" for p
+    using nonconstant[OF that] by (auto simp: Roots_def fundamental_theorem_of_algebra constant_degree)
+  have "Roots' \<noteq> {}"
+    using Roots_nonempty \<open>P \<noteq> {}\<close> by (auto simp: Roots'_def)
+  have "n > 0"
+    using \<open>Roots' \<noteq> {}\<close> \<open>finite Roots'\<close> by (auto simp: n_altdef)
+
+  text \<open>
+    We can split each polynomial in \<open>P\<close> into a product of linear factors:
+  \<close>
+  have of_int_poly_P:
+     "of_int_poly q = Polynomial.smult (Polynomial.lead_coeff q) (\<Prod>x\<in>Roots q. [:-x, 1:])"
+     if "q \<in> P" for q
+    using complex_poly_decompose_rsquarefree[OF rsquarefree[OF that]] by (simp add: Roots_def)
+
+  text \<open>
+    We let \<open>l\<close> be an integer such that $l\alpha$ is an algebraic integer for all our roots \<open>\<alpha>\<close>:
+  \<close>
+  define l where "l = (LCM q\<in>P. Polynomial.lead_coeff q)"
+  have alg_int: "algebraic_int (of_int l * x)" if "x \<in> Roots'" for x
+  proof -
+    from that obtain q where q: "q \<in> P" "ipoly q x = 0"
+      by (auto simp: Roots'_def Roots_def)
+    show ?thesis
+      by (rule algebraic_imp_algebraic_int'[of q]) (use q in \<open>auto simp: l_def\<close>)
+  qed
+  have "l \<noteq> 0"
+    using \<open>finite P\<close> by (auto simp: l_def Lcm_0_iff)
+  moreover have "l \<ge> 0"
+    unfolding l_def by (rule Lcm_int_greater_eq_0)
+  ultimately have "l > 0" by linarith
+
+  text \<open>
+    We can split the product of all the polynomials in \<open>P\<close> into linear factors:
+  \<close>
+  define lc_factor where "lc_factor = (\<Prod>q\<in>P. l ^ Polynomial.degree q div Polynomial.lead_coeff q)"
+  have lc_factor: "Polynomial.smult (of_int l ^ n) (\<Prod>\<alpha>'\<in>Roots'. [:-\<alpha>',1:]) =
+                      of_int_poly (Polynomial.smult lc_factor (\<Prod>P))"
+  proof -
+    define lc where "lc = (\<lambda>q. Polynomial.lead_coeff q :: int)"
+    define d where "d = (Polynomial.degree :: int poly \<Rightarrow> nat)"
+    have "(\<Prod>q\<in>P. of_int_poly q) =
+          (\<Prod>q\<in>P. Polynomial.smult (lc q) (\<Prod>x\<in>Roots q. [:-x, 1:]) :: complex poly)"
+      unfolding lc_def by (intro prod.cong of_int_poly_P refl)
+    also have "\<dots> = Polynomial.smult (\<Prod>q\<in>P. lc q) (\<Prod>q\<in>P. (\<Prod>x\<in>Roots q. [:-x, 1:]))"
+      by (simp add: prod_smult)
+    also have "(\<Prod>q\<in>P. (\<Prod>x\<in>Roots q. [:-x, 1:])) = (\<Prod>x\<in>Roots'. [:-x, 1:])"
+      unfolding Roots'_def using disjoint
+      by (intro prod.UNION_disjoint [symmetric]) (auto simp: disjoint_family_on_def)
+    also have "Polynomial.smult (of_int lc_factor) (Polynomial.smult (\<Prod>q\<in>P. lc q) \<dots>) =
+               Polynomial.smult (\<Prod>q\<in>P. of_int (l ^ d q div lc q * lc q)) (\<Prod>x\<in>Roots'. pCons (- x) 1)"
+      by (simp add: lc_factor_def prod.distrib lc_def d_def)
+    also have "(\<Prod>q\<in>P. of_int (l ^ d q div lc q * lc q)) = (\<Prod>q\<in>P. of_int l ^ d q :: complex)"
+    proof (intro prod.cong, goal_cases)
+      case (2 q)
+      have "lc q dvd l"
+        unfolding l_def lc_def using 2 by auto
+      also have "\<dots> dvd l ^ d q"
+        using 2 nonconstant[of q] by (intro dvd_power) (auto simp: d_def)
+      finally show ?case by simp
+    qed auto
+    also have "\<dots> = l ^ (\<Sum>q\<in>P. d q)"
+      by (simp add: power_sum)
+    also have "(\<Sum>q\<in>P. d q) = (\<Sum>q\<in>P. n_roots q)"
+    proof (intro sum.cong, goal_cases)
+      case (2 q)
+      thus ?case using rsquarefree[OF 2]
+        by (subst (asm) rsquarefree_card_degree) (auto simp: d_def n_roots_def Roots_def)
+    qed auto
+    also have "\<dots> = n"
+      by (simp add: n_def)
+    finally show ?thesis
+      by (simp add: of_int_hom.map_poly_hom_smult of_int_poly_hom.hom_prod)
+  qed
+
+  text \<open>
+    We define \<open>R\<close> to be the radius of the smallest circle around the origin in which all our
+    roots lie:
+  \<close>
+  define R :: real where "R = Max (norm ` Roots')"
+  have R_ge: "R \<ge> norm \<alpha>" if "\<alpha> \<in> Roots'" for \<alpha>
+    unfolding R_def using that by (intro Max_ge) auto
+  have "R \<ge> 0"
+  proof -
+    from \<open>Roots' \<noteq> {}\<close> obtain \<alpha> where "\<alpha> \<in> Roots'"
+      by auto
+    have "0 \<le> norm \<alpha>"
+      by simp
+    also have "\<dots> \<le> R"
+      by (intro R_ge) fact
+    finally show "R \<ge> 0"
+      by simp
+  qed
+
+  text \<open>
+    Now the main part of the proof: for any sufficiently large prime \<open>p\<close>, our assumptions
+    imply $(p-1)! ^ n \leq C' l^{np} (2R)^{np-1}$ for some constant $C'$:    
+  \<close>
+  define C :: "nat \<Rightarrow> real" where "C = (\<lambda>p. l ^ (n * p) * (2*R) ^ (n * p - 1))"
+  define C' where
+    "C' = (\<Prod>x\<in>Roots'. \<Sum>q\<in>P. real_of_int \<bar>\<beta> q\<bar> * (\<Sum>\<alpha>\<in>Roots q. cmod \<alpha> * exp (cmod \<alpha>)))"
+
+  text \<open>
+    We commence with the proof of the main inequality.
+  \<close>
+  have ineq: "fact (p - 1) ^ n \<le> C' * C p ^ n"
+    if p: "prime p" 
+    and p_ineqs: "\<forall>q\<in>P. p > \<bar>\<beta> q\<bar>"
+                 "real p > norm (\<Prod>\<alpha>\<in>Roots'. of_int (l^n) * (\<Prod>x\<in>Roots'-{\<alpha>}. \<alpha> - x))"
+    for p :: nat
+  proof -
+    have "p > 1"
+      using prime_gt_1_nat[OF p] .
+
+    text \<open>
+      We define the polynomial function
+        \[f_i(X) = l^{np} \frac{\prod_\alpha (X-\alpha)^p}{X - \alpha_i}\]
+      where the product runs over all roots $\alpha$.
+    \<close>
+    define f_poly :: "complex \<Rightarrow> complex poly" where
+      "f_poly = (\<lambda>\<alpha>. Polynomial.smult (l^(n*p)) ((\<Prod>\<alpha>'\<in>Roots'. [:-\<alpha>', 1:]^p) div [:-\<alpha>, 1:]))"
+    have f_poly_altdef: "f_poly \<alpha> = Polynomial.smult (l^(n*p))
+                           ((\<Prod>\<alpha>'\<in>Roots'. [:-\<alpha>', 1:]^(if \<alpha>' = \<alpha> then p - 1 else p)))"
+      if "\<alpha> \<in> Roots'" for \<alpha>
+    proof -
+      have "(\<Prod>\<alpha>'\<in>Roots'. [:-\<alpha>', 1:] ^ (if \<alpha>'=\<alpha> then p-1 else p)) * [:-\<alpha>, 1:] =
+            [:- \<alpha>, 1:] ^ (p - 1) * (\<Prod>x\<in>Roots' - {\<alpha>}. [:- x, 1:] ^ p) * [:- \<alpha>, 1:]"
+        using that by (subst prod.If_eq) (auto simp: algebra_simps)
+      also have "\<dots> = (\<Prod>x\<in>Roots' - {\<alpha>}. [:- x, 1:] ^ p) * [:- \<alpha>, 1:] ^ Suc (p - 1)"
+        by (simp only: power_Suc mult_ac)
+      also have "Suc (p - 1) = p"
+        using \<open>p > 1\<close> by auto
+      also have "(\<Prod>x\<in>Roots' - {\<alpha>}. [:- x, 1:] ^ p) * [:- \<alpha>, 1:] ^ p = (\<Prod>x\<in>Roots'. [:- x, 1:] ^ p)"
+        using that by (subst prod.remove[of _ \<alpha>]) auto
+      finally have eq: "(\<Prod>\<alpha>'\<in>Roots'. [:-\<alpha>', 1:] ^ (if \<alpha>'=\<alpha> then p-1 else p)) * [:-\<alpha>, 1:] =
+                        (\<Prod>x\<in>Roots'. [:- x, 1:] ^ p)" .
+      show ?thesis
+        unfolding f_poly_def eq[symmetric] by (subst nonzero_mult_div_cancel_right) auto
+    qed
+  
+    define f :: "complex \<Rightarrow> complex \<Rightarrow> complex"
+      where "f = (\<lambda>\<alpha> x. l^(n*p) * (\<Prod>\<alpha>'\<in>Roots'. (x - \<alpha>')^(if \<alpha>' = \<alpha> then p - 1 else p)))"
+    have eval_f: "poly (f_poly \<alpha>) x = f \<alpha> x" if "\<alpha> \<in> Roots'" for \<alpha> x
+      using that by (simp add: f_poly_altdef poly_prod f_def)
+    have deg_f: "Polynomial.degree (f_poly \<alpha>) = n * p - 1" if "\<alpha> \<in> Roots'" for \<alpha>
+    proof -
+      have "Polynomial.degree (f_poly \<alpha>) = p - 1 + (n - 1) * p"
+        unfolding f_poly_altdef[OF that] using that \<open>l > 0\<close> \<open>finite Roots'\<close>
+        by (subst prod.If_eq) (auto simp: degree_prod_eq degree_power_eq degree_mult_eq n_altdef)
+      also have "p - 1 + (n - 1) * p = n * p - 1"
+        using \<open>n > 0\<close> \<open>p > 1\<close> by (cases n) auto
+      finally show ?thesis .
+    qed
+
+    text \<open>
+      Next, we define the function $I_i(z) = \int_0^z e^{z-t} f_i(t) \text{d}t$, and,
+      based on that, the numbers $J_i = \sum_{i=1}^m \beta_i \sum_{q_i(x) = 0} I_i(x)$,
+      and the number $J$, which is the product of all the $J_i$:
+    \<close>
+    define I :: "complex \<Rightarrow> complex \<Rightarrow> complex"
+      where "I = (\<lambda>\<alpha> x. lindemann_weierstrass_aux.I (f_poly \<alpha>) x)"
+    define J :: "complex \<Rightarrow> complex"
+      where "J = (\<lambda>\<alpha>. \<Sum>q\<in>P. \<beta> q * (\<Sum>x\<in>Roots q. I \<alpha> x))"
+
+    define J' :: complex
+      where "J' = (\<Prod>\<alpha>\<in>Roots'. J \<alpha>)"
+
+    text \<open>
+      Reusing some of the machinery from the proof that \<open>e\<close> is transcendental,
+      we find the following equality for $J_i$:
+    \<close>
+    have J_eq: "J \<alpha> = -(\<Sum>q\<in>P. of_int (\<beta> q) * (\<Sum>x\<in>Roots q. \<Sum>j<n*p. poly ((pderiv ^^ j) (f_poly \<alpha>)) x))"
+      if "\<alpha> \<in> Roots'" for \<alpha>
+    proof -
+      have "n * p \<ge> 1 * 2"
+        using \<open>n > 0\<close> \<open>p > 1\<close> by (intro mult_mono) auto
+      hence [simp]: "{..n*p-Suc 0} = {..<n*p}"
+        by auto
+      have "J \<alpha> = (\<Sum>q\<in>P. \<beta> q * (\<Sum>x\<in>Roots q. I \<alpha> x))"
+        unfolding J_def ..
+      also have "\<dots> = (\<Sum>q\<in>P. of_int (\<beta> q) * (\<Sum>x\<in>Roots q. exp x * (\<Sum>j<n*p. poly ((pderiv ^^ j) (f_poly \<alpha>)) 0))) -
+                      (\<Sum>q\<in>P. of_int (\<beta> q) * (\<Sum>x\<in>Roots q. \<Sum>j<n*p. poly ((pderiv ^^ j) (f_poly \<alpha>)) x))"
+        unfolding I_def lindemann_weierstrass_aux.I_def
+        by (simp add: deg_f that ring_distribs sum_subtractf sum_distrib_left sum_distrib_right mult_ac)
+      also have "\<dots> = -(\<Sum>q\<in>P. of_int (\<beta> q) * (\<Sum>x\<in>Roots q. \<Sum>j<n*p. poly ((pderiv ^^ j) (f_poly \<alpha>)) x))"
+        unfolding sum_distrib_right [symmetric] mult.assoc [symmetric] sum_eq_0 by simp
+      finally show ?thesis .
+    qed
+
+    text \<open>
+      The next big step is to show that $(p-1)! \mid J_i$ as an algebraic integer (i.e.
+      $J_i / (p-1)!$ is an algebraic integer), but $p \not\mid J_i$. This is done by brute force:
+      We show that every summand in the above sum has $p!$ as a factor, except for
+      the one corresponding to $x = \alpha_i$, $j = p - 1$, which has $(p-1)!$ as a factor but
+      not \<open>p\<close>.
+    \<close>
+    have J: "fact (p - 1) alg_dvd J \<alpha>" "\<not>of_nat p alg_dvd J \<alpha>" if \<alpha>: "\<alpha> \<in> Roots'" for \<alpha>
+    proof -
+      define h where "h = (\<lambda>\<alpha>' j. poly ((pderiv ^^ j) (f_poly \<alpha>)) \<alpha>')"
+      from \<alpha> obtain q where q: "q \<in> P" "\<alpha> \<in> Roots q"
+        by (auto simp: Roots'_def)
+  
+      have "J \<alpha> = -(\<Sum>(q, \<alpha>')\<in>Sigma P Roots. \<Sum>j<n*p. of_int (\<beta> q) * h \<alpha>' j)"
+        unfolding J_eq[OF \<alpha>] h_def sum_distrib_left by (subst (2) sum.Sigma) auto
+      also have "\<dots> = -(\<Sum>((q,\<alpha>'),i)\<in>Sigma P Roots\<times>{..<n*p}. of_int (\<beta> q) * h \<alpha>' i)"
+        by (subst (2) sum.Sigma [symmetric]) (auto simp: case_prod_unfold)
+      finally have J_eq': "J \<alpha> = - (\<Sum>((q, \<alpha>'), i)\<in>Sigma P Roots \<times> {..<n * p}. of_int (\<beta> q) * h \<alpha>' i)" .
+  
+      have h_\<alpha>_pm1_eq: "h \<alpha> (p-1) = of_int (l^(n*p)) * fact (p-1) * (\<Prod>\<alpha>'\<in>Roots'-{\<alpha>}. (\<alpha>-\<alpha>')^p)"
+      proof -
+        have "h \<alpha> (p - 1) = of_int (l ^ (n * p)) *
+                poly ((pderiv ^^ (p-1)) (\<Prod>\<alpha>'\<in>Roots'. [:-\<alpha>',1:] ^ (if \<alpha>' = \<alpha> then p - 1 else p))) \<alpha>"
+          unfolding h_def f_poly_altdef[OF \<alpha>] higher_pderiv_smult poly_smult ..
+        also have "(\<Prod>\<alpha>'\<in>Roots'. [:-\<alpha>',1:] ^ (if \<alpha>' = \<alpha> then p - 1 else p)) =
+                    [:-\<alpha>,1:]^(p-1) * (\<Prod>\<alpha>'\<in>Roots'-{\<alpha>}. [:-\<alpha>',1:]^p)"
+          using \<alpha> by (subst prod.If_eq) auto
+        also have "poly ((pderiv ^^ (p-1)) \<dots>) \<alpha> = fact (p - 1) * (\<Prod>\<alpha>'\<in>Roots' - {\<alpha>}. (\<alpha> - \<alpha>') ^ p)"
+          by (subst poly_higher_pderiv_aux2) (simp_all add: poly_prod)
+        finally show ?thesis by (simp only: mult.assoc)
+      qed
+  
+      have "fact (p-1) alg_dvd h \<alpha> (p-1)"
+      proof -
+        have "fact (p-1) alg_dvd fact (p-1) * (of_int (l^p) * (\<Prod>\<alpha>'\<in>Roots'-{\<alpha>}. (l*\<alpha>-l*\<alpha>')^p))"
+          by (intro alg_dvd_triv_left algebraic_int_times[of "of_int (l^p)"]
+                    algebraic_int_prod algebraic_int_power algebraic_int_diff
+                    alg_int \<alpha> algebraic_int_of_int) auto
+        also have "(\<Prod>\<alpha>'\<in>Roots'-{\<alpha>}. (l*\<alpha>-l*\<alpha>')^p) = (\<Prod>\<alpha>'\<in>Roots'-{\<alpha>}. of_int l^p * (\<alpha>-\<alpha>')^p)"
+          by (subst power_mult_distrib [symmetric]) (simp_all add: algebra_simps)
+        also have "\<dots> = of_int (l ^ (p * (n-1))) * (\<Prod>\<alpha>'\<in>Roots'-{\<alpha>}. (\<alpha>-\<alpha>')^p)"
+          using \<alpha> by (subst prod.distrib) (auto simp: card_Diff_subset n_altdef simp flip: power_mult)
+        also have "of_int (l^p) * \<dots> = of_int (l^(p+p*(n-1))) * (\<Prod>\<alpha>'\<in>Roots'-{\<alpha>}. (\<alpha>-\<alpha>')^p)"
+          unfolding mult.assoc [symmetric] power_add [symmetric] of_int_power ..
+        also have "p + p * (n - 1) = n * p"
+          using \<open>n > 0\<close> by (cases n) (auto simp: mult_ac)
+        also have "fact (p - 1) * (of_int (l^(n*p)) * (\<Prod>\<alpha>'\<in>Roots'-{\<alpha>}. (\<alpha>-\<alpha>')^p)) = h \<alpha> (p-1)"
+          unfolding h_\<alpha>_pm1_eq by (simp add: mult_ac)
+        finally show ?thesis .
+      qed
+ 
+      have "\<not>of_nat p alg_dvd of_int (\<beta> q) * h \<alpha> (p-1)"
+        unfolding h_\<alpha>_pm1_eq mult.assoc [symmetric] of_int_mult [symmetric]
+      proof
+        define r where "r = (\<lambda>\<alpha>. of_int (l^n) * (\<Prod>\<alpha>'\<in>Roots'-{\<alpha>}. \<alpha>-\<alpha>'))"
+        have alg_int_r: "algebraic_int (r \<alpha>)" if "\<alpha> \<in> Roots'" for \<alpha>
+        proof -
+          have "algebraic_int (of_int l * (\<Prod>\<alpha>'\<in>Roots'-{\<alpha>}. of_int l * \<alpha> - of_int l * \<alpha>'))"
+            by (intro algebraic_int_times[OF algebraic_int_of_int] algebraic_int_prod 
+                      algebraic_int_power algebraic_int_diff alg_int that) auto
+          also have "\<dots> = of_int l * (\<Prod>\<alpha>'\<in>Roots'-{\<alpha>}. of_int l * (\<alpha> - \<alpha>'))"
+            by (simp add: algebra_simps flip: power_mult_distrib)
+          also have "\<dots> = of_int (l^(1 + (n-1))) * (\<Prod>\<alpha>'\<in>Roots'-{\<alpha>}. \<alpha> - \<alpha>')"
+            using that by (simp add: r_def prod.distrib card_Diff_subset
+                                     n_altdef power_add mult_ac flip: power_mult)
+          also have "1 + (n - 1) = n"
+            using \<open>n > 0\<close> by auto
+          finally show "algebraic_int (r \<alpha>)"
+            unfolding r_def .
+        qed
+
+        have "(\<Prod>\<alpha>'\<in>Roots'. r \<alpha>') \<in> \<rat>"
+        proof -
+          obtain Root where Root_bij: "bij_betw Root {..<n} Roots'"
+            using ex_bij_betw_nat_finite[OF \<open>finite Roots'\<close>] unfolding n_altdef atLeast0LessThan by metis
+          have Root_in_Roots': "Root i \<in> Roots'" if "i < n" for i
+            using Root_bij that by (auto simp: bij_betw_def)
+
+          define R :: "complex mpoly" where
+            "R = (\<Prod>i<n. Const (of_int (l^n)) * (\<Prod>j\<in>{..<n}-{i}. Var i - Var j))"
+          have "insertion Root R \<in> \<rat>"
+          proof (rule symmetric_poly_of_roots_in_subring)
+            show "symmetric_mpoly {..<n} R"
+              unfolding R_def
+            proof (rule symmetric_mpoly_symmetric_prod'[of _ "\<lambda>\<pi>. \<pi>"], goal_cases)
+              case (2 i \<pi>)
+              from \<open>\<pi> permutes {..<n}\<close> have [simp]: "bij \<pi>"
+                by (rule permutes_bij)
+              have "mpoly_map_vars \<pi> (Const (of_int (l ^ n)) *
+                      (\<Prod>j\<in>{..<n} - {i}. Var i - Var j):: complex mpoly) =
+                    Const (of_int l ^ n) * (\<Prod>j\<in>{..<n} - {i}. Var (\<pi> i) - Var (\<pi> j))"
+                by simp
+              also have "(\<Prod>j\<in>{..<n} - {i}. Var (\<pi> i) - Var (\<pi> j)) =
+                         (\<Prod>j\<in>{..<n} - {\<pi> i}. Var (\<pi> i) - Var j)"
+                using 2 permutes_in_image[OF 2(2), of i]
+                by (intro prod.reindex_bij_betw bij_betw_Diff permutes_imp_bij[OF 2(2)])
+                   (auto simp: bij_betw_singleton)
+              finally show ?case by simp
+            qed
+          next
+            show "vars R \<subseteq> {..<n}" unfolding R_def
+              by (intro order.trans[OF vars_prod] UN_least order.trans[OF vars_mult]
+                        Un_least order.trans[OF vars_power] order.trans[OF vars_diff])
+                 (auto simp: vars_Var)
+          next
+            show "ring_closed (\<rat> :: complex set)"
+              by unfold_locales auto
+            then interpret ring_closed "\<rat> :: complex set" .              
+            show "\<forall>m. MPoly_Type.coeff R m \<in> \<rat>"
+              unfolding R_def
+              by (intro allI coeff_prod_closed coeff_mult_closed coeff_power_closed)
+                 (auto simp: mpoly_coeff_Const coeff_Var when_def)
+          next
+            let ?lc = "of_int (\<Prod>p\<in>P. Polynomial.lead_coeff p) :: complex"
+            have "(\<Prod>q\<in>P. of_int_poly q) = (\<Prod>q\<in>P. Polynomial.smult
+                    (of_int (Polynomial.lead_coeff q)) (\<Prod>x\<in>Roots q. [:-x, 1:]))"
+              by (intro prod.cong of_int_poly_P refl)
+            also have "\<dots> = Polynomial.smult ?lc (\<Prod>q\<in>P. \<Prod>x\<in>Roots q. [:-x, 1:])"
+              by (simp add: prod_smult)
+            also have "(\<Prod>q\<in>P. \<Prod>x\<in>Roots q. [:-x, 1:]) = (\<Prod>x\<in>Roots'. [:-x, 1:])"
+              unfolding Roots'_def using disjoint
+              by (intro prod.UNION_disjoint [symmetric]) (auto simp: disjoint_family_on_def)
+            also have "\<dots> = (\<Prod>i<n. [:- Root i, 1:])"
+              by (intro prod.reindex_bij_betw [symmetric] Root_bij)
+            finally show "of_int_poly (\<Prod>P) = Polynomial.smult ?lc (\<Prod>i<n. [:- Root i, 1:])"
+              by (simp add: of_int_poly_hom.hom_prod)
+            have "prod Polynomial.lead_coeff P \<noteq> 0"
+              by (intro prod_nonzeroI) auto
+            thus "inverse ?lc * ?lc = 1" "inverse ?lc \<in> \<rat>"
+              by (auto simp: field_simps simp flip: of_int_prod)
+          qed auto
+          also have "insertion Root R = (\<Prod>i<n. of_int (l^n) * (\<Prod>j\<in>{..<n}-{i}. Root i - Root j))"
+            by (simp add: R_def insertion_prod insertion_mult insertion_power insertion_diff)
+          also have "\<dots> = (\<Prod>i<n. of_int (l^n) * (\<Prod>\<alpha>'\<in>Roots'-{Root i}. Root i - \<alpha>'))"
+          proof (intro prod.cong, goal_cases)
+            case (2 i)
+            hence "(\<Prod>j\<in>{..<n}-{i}. Root i - Root j) = (\<Prod>\<alpha>'\<in>Roots'-{Root i}. Root i - \<alpha>')"
+              by (intro prod.reindex_bij_betw bij_betw_Diff Root_bij)
+                 (auto intro: Root_in_Roots' simp: bij_betw_singleton)
+            thus ?case by simp
+          qed auto
+          also have "\<dots> = (\<Prod>\<alpha>'\<in>Roots'. r \<alpha>')"
+            unfolding r_def by (intro prod.reindex_bij_betw Root_bij)
+          finally show "(\<Prod>\<alpha>'\<in>Roots'. r \<alpha>') \<in> \<rat>" .
+        qed
+        moreover have "algebraic_int (\<Prod>\<alpha>'\<in>Roots'. r \<alpha>')"
+          by (intro algebraic_int_prod alg_int_r)
+        ultimately have is_int: "(\<Prod>\<alpha>'\<in>Roots'. r \<alpha>') \<in> \<int>"
+          using rational_algebraic_int_is_int by blast
+        then obtain R' where R': "(\<Prod>\<alpha>'\<in>Roots'. r \<alpha>') = of_int R'"
+          by (elim Ints_cases)
+        have "(\<Prod>\<alpha>'\<in>Roots'. r \<alpha>') \<noteq> 0"
+          using \<open>l > 0\<close> by (intro prod_nonzeroI) (auto simp: r_def \<open>finite Roots'\<close>)
+        with R' have [simp]: "R' \<noteq> 0"
+          by auto
+
+        assume "of_nat p alg_dvd of_int (\<beta> q * l^(n*p)) * fact (p-1) * (\<Prod>\<alpha>'\<in>Roots'-{\<alpha>}. (\<alpha>-\<alpha>') ^ p)"
+        also have "\<dots> = of_int (\<beta> q) * fact (p-1) * r \<alpha> ^ p"
+          by (simp add: r_def mult_ac power_mult_distrib power_mult prod_power_distrib)
+        also have "\<dots> alg_dvd of_int (\<beta> q) * fact (p-1) * r \<alpha> ^ p * (\<Prod>\<alpha>'\<in>Roots'-{\<alpha>}. r \<alpha>') ^ p"
+          by (intro alg_dvd_triv_left algebraic_int_prod alg_int_r algebraic_int_power) auto
+        also have "\<dots> = of_int (\<beta> q) * fact (p-1) * (\<Prod>\<alpha>'\<in>Roots'. r \<alpha>') ^ p"
+          using \<alpha> by (subst (2) prod.remove[of _ "\<alpha>"]) (auto simp: mult_ac power_mult_distrib)
+        also have "\<dots> = of_int (\<beta> q * fact (p - 1) * R' ^ p)"
+          by (simp add: R')
+        also have "of_nat p = of_int (int p)"
+          by simp
+        finally have "int p dvd \<beta> q * fact (p - 1) * R' ^ p" 
+          by (subst (asm) alg_dvd_of_int_iff)
+        moreover have "prime (int p)"
+          using \<open>prime p\<close> by auto
+        ultimately have "int p dvd \<beta> q \<or> int p dvd fact (p - 1) \<or> int p dvd R' ^ p"
+          by (simp add: prime_dvd_mult_iff)
+        moreover have "\<not>int p dvd \<beta> q"
+        proof
+          assume "int p dvd \<beta> q"
+          hence "int p \<le> \<bar>\<beta> q\<bar>"
+            using \<beta>_nz[of q] dvd_imp_le_int[of "\<beta> q" "int p"] q by auto
+          with p_ineqs(1) q show False by auto
+        qed
+        moreover have "\<not>int p dvd fact (p - 1)"
+        proof -
+          have "\<not>p dvd fact (p - 1)"
+            using \<open>p > 1\<close> p by (subst prime_dvd_fact_iff) auto
+          hence "\<not>int p dvd int (fact (p - 1))"
+            by (subst int_dvd_int_iff)
+          thus ?thesis unfolding of_nat_fact .
+        qed
+        moreover have "\<not>int p dvd R' ^ p"
+        proof
+          assume "int p dvd R' ^ p"
+          hence "int p dvd R'"
+            using \<open>prime (int p)\<close> prime_dvd_power by metis
+          hence "int p \<le> \<bar>R'\<bar>"
+            using \<beta>_nz[of q] dvd_imp_le_int[of R' "int p"] q by auto
+          hence "real p \<le> real_of_int \<bar>R'\<bar>"
+            by linarith
+          also have "\<dots> = norm (\<Prod>\<alpha>\<in>Roots'. r \<alpha>)"
+            unfolding R' by simp
+          finally show False unfolding r_def using p_ineqs(2)
+            by linarith
+        qed
+        ultimately show False
+          by blast
+      qed
+  
+      have fact_p_dvd: "fact p alg_dvd h \<alpha>' j" if "\<alpha>' \<in> Roots'" "\<alpha>' \<noteq> \<alpha> \<or> j \<noteq> p - 1" for \<alpha>' j
+      proof (cases "j \<ge> p")
+        case False
+        with that have j: "j < (if \<alpha>' = \<alpha> then p - 1 else p)"
+          by auto
+        have "h \<alpha>' j = 0"
+          unfolding h_def f_poly_altdef[OF \<alpha>]
+          by (intro poly_higher_pderiv_aux1'[OF j] dvd_smult dvd_prodI that) auto
+        thus ?thesis by simp
+      next
+        case True
+        define e where "e = (\<lambda>x. if x = \<alpha> then p - 1 else p)"
+        define Q where "Q = (\<Prod>x\<in>Roots'. [:-x, 1:] ^ e x)"
+        define Q' where "Q' = Polynomial.smult (of_int (l^(n*p+j))) (pcompose Q [:0, 1 / of_int l:])"
+        have "poly ((pderiv ^^ j) Q) \<alpha>' / l ^ j =
+                poly ((pderiv ^^ j) (pcompose Q [:0, 1 / of_int l:])) (l * \<alpha>')"
+          using \<open>l > 0\<close> by (simp add: higher_pderiv_pcompose_linear poly_pcompose field_simps)
+
+        have "sum e Roots' = (n - 1) * p + (p - 1)"
+          unfolding e_def using \<alpha>
+          by (subst sum.If_eq) (auto simp: card_Diff_subset n_altdef algebra_simps)
+        also have "\<dots> = n * p - 1"
+          using \<open>n > 0\<close> \<open>p > 1\<close> by (cases n) auto
+        finally have [simp]: "sum e Roots' = n * p - 1" .
+
+        have "h \<alpha>' j = of_int (l^(n*p)) * poly ((pderiv ^^ j) Q) \<alpha>'"
+          unfolding h_def f_poly_altdef[OF \<alpha>] higher_pderiv_smult poly_smult e_def Q_def ..
+        also have "poly ((pderiv ^^ j) Q) \<alpha>' =
+                     of_int l ^ j * poly ((pderiv ^^ j) (pcompose Q [:0, 1 / of_int l:])) (l * \<alpha>')"
+          using \<open>l > 0\<close> by (simp add: higher_pderiv_pcompose_linear poly_pcompose field_simps)
+        also have "of_int (l ^ (n * p)) * \<dots> = poly ((pderiv ^^ j) Q') (l * \<alpha>')"
+          by (simp add: Q'_def higher_pderiv_smult power_add)
+        also have "fact p alg_dvd \<dots>"
+        proof (rule fact_alg_dvd_poly_higher_pderiv)
+          show "j \<ge> p" by fact
+          show "algebraic_int (of_int l * \<alpha>')"
+            by (rule alg_int) fact
+          interpret alg_int: ring_closed "{x::complex. algebraic_int x}"
+            by standard auto
+          show "algebraic_int (poly.coeff Q' i)" for i
+          proof (cases "i \<le> Polynomial.degree Q'")
+            case False
+            thus ?thesis
+              by (simp add: coeff_eq_0)
+          next
+            case True
+            hence "i \<le> n * p - 1" using \<open>l > 0\<close>
+              by (simp add: Q'_def degree_prod_eq Q_def degree_power_eq)
+            also have "n * p > 0"
+              using \<open>n > 0\<close> \<open>p > 1\<close> by auto
+            hence "n * p - 1 < n * p"
+              by simp
+            finally have i: "i < n * p" .
+
+            have "poly.coeff Q' i = of_int l ^ (n * p + j) / of_int l ^ i * poly.coeff Q i"
+              by (simp add: Q'_def coeff_pcompose_linear field_simps)
+            also have "of_int l ^ (n * p + j) = (of_int l ^ (n * p + j - i) :: complex) * of_int l ^ i"
+              unfolding power_add [symmetric] using i by simp
+            hence "of_int l ^ (n * p + j) / of_int l ^ i = (of_int l ^ (n * p + j - i) :: complex)"
+              using \<open>l > 0\<close> by (simp add: field_simps)
+            also have "\<dots> * poly.coeff Q i =
+                (\<Sum>X\<in>{X. X \<subseteq> (SIGMA x:Roots'. {..<e x}) \<and> i = n * p - Suc (card X)}.
+                of_int l ^ (n * p + j - (n * p - Suc (card X))) * ((- 1) ^ card X * prod fst X))"
+              unfolding Q_def by (subst coeff_prod_linear_factors) (auto simp: sum_distrib_left)
+            also have "algebraic_int \<dots>"
+            proof (intro algebraic_int_sum, goal_cases)
+              case (1 X)
+              hence X: "X \<subseteq> (SIGMA x:Roots'. {..<e x})"
+                by auto
+              have card_eq: "card (SIGMA x:Roots'. {..<e x}) = n * p - 1"
+                by (subst card_SigmaI) auto
+              from X have "card X \<le> card (SIGMA x:Roots'. {..<e x})"
+                by (intro card_mono) auto
+              hence "card X \<le> n * p - 1"
+                using card_eq by auto
+              also have "\<dots> < n * p"
+                using  \<open>n * p > 0\<close> by simp
+              finally have card_less: "card X < n * p" .
+              have "algebraic_int ((-1) ^ card X * of_int l ^ (j + 1) * (\<Prod>x\<in>X. of_int l * fst x))"
+                using X by (intro algebraic_int_times algebraic_int_prod alg_int) auto
+              thus ?case
+                using card_less by (simp add: power_add prod.distrib mult_ac)
+            qed
+            finally show ?thesis .
+          qed
+        qed
+        finally show ?thesis .
+      qed
+  
+      have p_dvd: "of_nat p alg_dvd h \<alpha>' j" if "\<alpha>' \<in> Roots'" "\<alpha>' \<noteq> \<alpha> \<or> j \<noteq> p - 1" for \<alpha>' j
+      proof -
+        have "of_nat p alg_dvd (of_nat (fact p) :: complex)"
+          by (intro alg_dvd_of_nat dvd_fact) (use \<open>p > 1\<close> in auto)
+        hence "of_nat p alg_dvd (fact p :: complex)"
+          by simp
+        also have "\<dots> alg_dvd h \<alpha>' j"
+          using that by (intro fact_p_dvd)
+        finally show ?thesis .
+      qed
+  
+      show "fact (p - 1) alg_dvd J \<alpha>"
+        unfolding J_eq'
+      proof (intro alg_dvd_uminus_right alg_dvd_sum, safe intro!: alg_dvd_mult algebraic_int_of_int)
+        fix q \<alpha>' j
+        assume "q \<in> P" "\<alpha>' \<in> Roots q" "j < n * p"
+        hence "\<alpha>' \<in> Roots'"
+          by (auto simp: Roots'_def)
+        show "fact (p - 1) alg_dvd h \<alpha>' j"
+        proof (cases "\<alpha>' = \<alpha> \<and> j = p - 1")
+          case True
+          thus ?thesis using \<open>fact (p - 1) alg_dvd h \<alpha> (p - 1)\<close>
+            by simp
+        next
+          case False
+          have "of_int (fact (p - 1)) alg_dvd (of_int (fact p) :: complex)"
+            by (intro alg_dvd_of_int fact_dvd) auto
+          hence "fact (p - 1) alg_dvd (fact p :: complex)"
+            by simp
+          also have "\<dots> alg_dvd h \<alpha>' j"
+            using False \<open>\<alpha>' \<in> Roots'\<close> by (intro fact_p_dvd) auto
+          finally show ?thesis .
+        qed
+      qed
+  
+      show "\<not>of_nat p alg_dvd J \<alpha>"
+        unfolding J_eq' alg_dvd_uminus_right_iff
+      proof (rule not_alg_dvd_sum)
+        have "p - 1 < 1 * p"
+          using \<open>p > 1\<close> by simp
+        also have "1 * p \<le> n * p"
+          using \<open>n > 0\<close> by (intro mult_right_mono) auto
+        finally show "((q, \<alpha>), p - 1) \<in> Sigma P Roots \<times> {..<n*p}"
+          using q \<open>n > 0\<close> by auto
+      next
+        fix z assume z: "z \<in> Sigma P Roots \<times> {..<n*p}-{((q,\<alpha>),p-1)}"
+        from z have "snd (fst z) \<in> Roots'"
+          by (auto simp: Roots'_def)
+        moreover have "fst (fst z) = q" if "\<alpha> \<in> Roots (fst (fst z))"
+        proof -
+          have "\<alpha> \<in> Roots (fst (fst z)) \<inter> Roots q" "q \<in> P" "fst (fst z) \<in> P"
+            using that q z by auto
+          with disjoint show ?thesis
+            unfolding disjoint_family_on_def by blast
+        qed
+        ultimately have "of_nat p alg_dvd h (snd (fst z)) (snd z)"
+          using z by (intro p_dvd) auto
+        thus  "of_nat p alg_dvd (case z of (x, xa) \<Rightarrow> (case x of (q, \<alpha>') \<Rightarrow> \<lambda>i. of_int (\<beta> q) * h \<alpha>' i) xa)"
+          using z by auto
+      qed (use \<open>\<not>of_nat p alg_dvd of_int (\<beta> q) * h \<alpha> (p-1)\<close> in auto)
+    qed
+
+    text \<open>
+      Our next goal is to show that $J$ is rational. This is done by repeated applications
+      of the fundamental theorem of symmetric polynomials, exploiting the fact that $J$ is
+      symmetric in all the $\alpha_i$ for each set of conjugates.
+    \<close>
+    define g :: "int poly poly"
+      where "g = synthetic_div (map_poly (\<lambda>x. [:x:])
+                   ((Polynomial.smult lc_factor (\<Prod>P)) ^ p)) [:0, 1:]"
+    have g: "map_poly (\<lambda>p. ipoly p \<alpha>) g = f_poly \<alpha>" if \<alpha>: "\<alpha> \<in> Roots'" for \<alpha>
+    proof -
+      interpret \<alpha>: comm_ring_hom "\<lambda>p. ipoly p \<alpha>"
+        by standard (auto simp: of_int_hom.poly_map_poly_eval_poly of_int_poly_hom.hom_mult)
+      define Q :: "int poly" where "Q = (Polynomial.smult lc_factor (\<Prod>P)) ^ p"
+      have "f_poly \<alpha> = Polynomial.smult (of_int (l^(n*p))) ((\<Prod>\<alpha>'\<in>Roots'. [:-\<alpha>',1:])^p) div [:-\<alpha>,1:]"
+        unfolding f_poly_def div_smult_left [symmetric] prod_power_distrib[symmetric] ..
+      also have "of_int (l^(n*p)) = (of_int l^n)^p"
+        by (simp add: power_mult)
+      also have "Polynomial.smult \<dots> ((\<Prod>\<alpha>'\<in>Roots'. [:-\<alpha>',1:])^p) =
+                   (Polynomial.smult (of_int l ^ n) (\<Prod>\<alpha>'\<in>Roots'. [:-\<alpha>',1:])) ^ p"
+        by (simp only: smult_power)
+      also have "\<dots> = of_int_poly Q"
+        by (subst lc_factor) (simp_all add: Q_def of_int_poly_hom.hom_power)
+      also have "\<dots> div [:-\<alpha>, 1:] = synthetic_div (of_int_poly Q) \<alpha>"
+        unfolding synthetic_div_altdef ..
+      also have "\<dots> = synthetic_div (map_poly (\<lambda>p. ipoly p \<alpha>) (map_poly (\<lambda>x. [:x:]) Q)) (ipoly [:0, 1:] \<alpha>)"
+        by (simp add: map_poly_map_poly o_def)
+      also have "\<dots> = map_poly (\<lambda>p. ipoly p \<alpha>) g"
+        unfolding g_def Q_def by (rule \<alpha>.synthetic_div_hom)
+      finally show ?thesis ..
+    qed
+
+    obtain Q where Q: "J \<alpha> = -(\<Sum>q\<in>P. of_int (\<beta> q) * eval_poly of_rat (Q q) \<alpha>)"
+      if "\<alpha> \<in> Roots'" for \<alpha>
+    proof -
+      define g' :: "nat \<Rightarrow> complex poly poly"
+        where "g' = (\<lambda>j.  (map_poly of_int_poly ((pderiv ^^ j) g)))"
+      obtain root :: "int poly \<Rightarrow> nat \<Rightarrow> complex"
+        where root: "\<And>q. q \<in> P \<Longrightarrow> bij_betw (root q) {..<\<sharp>q} (Roots q)"
+        using ex_bij_betw_nat_finite[OF finite_Roots] unfolding n_roots_def atLeast0LessThan
+        by metis
+      have "\<exists>Q'. map_poly of_rat Q' = (\<Sum>x\<in>Roots q. poly (g' j) [:x:])" if q: "q \<in> P" for q j
+      proof -
+        define Q :: "nat \<Rightarrow> complex poly mpoly"
+          where "Q = (\<lambda>j. (\<Sum>i<\<sharp>q. mpoly_of_poly i (g' j)))"
+        define ratpolys :: "complex poly set" where "ratpolys = {p. \<forall>i. poly.coeff p i \<in> \<rat>}"
+        have "insertion ((\<lambda>x. [:x:]) \<circ> root q) (Q j) \<in> ratpolys"
+        proof (rule symmetric_poly_of_roots_in_subring)
+          show "ring_closed ratpolys"
+            by standard (auto simp: ratpolys_def intro!: coeff_mult_semiring_closed)
+          show "\<forall>m. MPoly_Type.coeff (Q j) m \<in> ratpolys"
+            by (auto simp: Q_def ratpolys_def Polynomial.coeff_sum coeff_mpoly_of_poly when_def g'_def
+                     intro!: sum_in_Rats)
+          show "vars (Q j) \<subseteq> {..<\<sharp>q}" unfolding Q_def
+            by (intro order.trans[OF vars_sum] UN_least order.trans[OF vars_mpoly_of_poly]) auto
+          show "symmetric_mpoly {..<\<sharp>q} (Q j)" unfolding Q_def
+            by (rule symmetric_mpoly_symmetric_sum[of _ id]) (auto simp: permutes_bij)
+          interpret coeff_lift_hom: map_poly_idom_hom "\<lambda>x. [:x:]"
+            by standard
+          define lc :: complex where "lc = of_int (Polynomial.lead_coeff q)"
+          have "of_int_poly q = Polynomial.smult (Polynomial.lead_coeff q) (\<Prod>x\<in>Roots q. [:-x, 1:])"
+            by (rule of_int_poly_P) fact
+          also have "poly_lift \<dots> = Polynomial.smult [:lc:] (\<Prod>a\<in>Roots q. [:-[:a:], 1:])"
+            by (simp add: poly_lift_def map_poly_smult coeff_lift_hom.hom_prod lc_def)
+          also have "(\<Prod>a\<in>Roots q. [:-[:a:], 1:]) = (\<Prod>i<\<sharp>q. [:-[:root q i:], 1:])"
+            by (intro prod.reindex_bij_betw [symmetric] root q)
+          also have "\<dots> = (\<Prod>i<\<sharp>q. [:- ((\<lambda>x. [:x:]) \<circ> root q) i, 1:])"
+            by simp
+          finally show "poly_lift (Ring_Hom_Poly.of_int_poly q) = Polynomial.smult [:lc:] \<dots>" .
+          have "lc \<noteq> 0"
+            using q by (auto simp: lc_def)
+          thus "[:inverse lc:] * [:lc:] = 1"
+            by (simp add: field_simps)
+        qed (auto simp: ratpolys_def coeff_pCons split: nat.splits)
+
+        also have "insertion ((\<lambda>x. [:x:]) \<circ> root q) (Q j) = (\<Sum>i<\<sharp>q. poly (g' j) [:root q i:])"
+          by (simp add: Q_def insertion_sum poly_sum)
+        also have "\<dots> = (\<Sum>x\<in>Roots q. poly (g' j) [:x:])"
+          by (intro sum.reindex_bij_betw root q)
+        finally have "\<forall>i. poly.coeff (\<Sum>x\<in>Roots q. poly (g' j) [:x:]) i \<in> \<rat>"
+          by (auto simp: ratpolys_def)
+        thus ?thesis
+          using ratpolyE by metis
+      qed
+      then obtain Q where Q: "\<And>q j. q \<in> P \<Longrightarrow> map_poly of_rat (Q q j) = (\<Sum>x\<in>Roots q. poly (g' j) [:x:])"
+        by metis
+      define Q' where "Q' = (\<lambda>q. \<Sum>j<n*p. Q q j)"
+
+      have "J \<alpha> = - (\<Sum>q\<in>P. of_int (\<beta> q) * eval_poly of_rat (Q' q) \<alpha>)" if \<alpha>: "\<alpha> \<in> Roots'" for \<alpha>
+      proof -
+        have "J \<alpha> = -(\<Sum>q\<in>P. of_int (\<beta> q) * (\<Sum>x\<in>Roots q. \<Sum>j<n * p. poly ((pderiv ^^ j) (f_poly \<alpha>)) x))"
+          (is "_ = -?S") unfolding J_eq[OF \<alpha>] ..
+        also have "?S = (\<Sum>q\<in>P. of_int (\<beta> q) * eval_poly of_rat (Q' q) \<alpha>)"
+        proof (rule sum.cong, goal_cases)
+          case q: (2 q)
+          interpret \<alpha>: idom_hom "\<lambda>p. ipoly p \<alpha>"
+            by standard (auto simp: of_int_hom.poly_map_poly_eval_poly of_int_poly_hom.hom_mult)
+  
+          have "(\<Sum>x\<in>Roots q. \<Sum>j<n * p. poly ((pderiv ^^ j) (f_poly \<alpha>)) x) =
+                (\<Sum>j<n * p. \<Sum>x\<in>Roots q. poly ((pderiv ^^ j) (f_poly \<alpha>)) x)"
+            by (rule sum.swap)
+          also have "\<dots> = (\<Sum>j<n * p. eval_poly of_rat (Q q j) \<alpha>)"
+          proof (rule sum.cong, goal_cases)
+            case j: (2 j)
+            have "(\<Sum>x\<in>Roots q. poly ((pderiv ^^ j) (f_poly \<alpha>)) x) =
+                  (\<Sum>x\<in>Roots q. poly (poly (g' j) [:x:]) \<alpha>)"
+            proof (rule sum.cong, goal_cases)
+              case (2 x)
+              have "poly ((pderiv ^^ j) (f_poly \<alpha>)) x =
+                    poly ((pderiv ^^ j) (map_poly (\<lambda>p. ipoly p \<alpha>) g)) x"
+                by (subst g[OF \<alpha>, symmetric]) (rule refl)
+              also have "\<dots> = poly (eval_poly ((\<lambda>p. [:poly p \<alpha>:]) \<circ> of_int_poly) ((pderiv ^^ j) g) [:0, 1:]) x"
+                unfolding o_def \<alpha>.map_poly_higher_pderiv [symmetric]
+                by (simp only: \<alpha>.map_poly_eval_poly)
+              also have "\<dots> = poly (eval_poly (\<lambda>p. [:poly p \<alpha>:])
+                                (map_poly of_int_poly ((pderiv ^^ j) g)) [:0, 1:]) x"
+                unfolding eval_poly_def by (subst map_poly_map_poly) auto
+              also have "\<dots> = poly (poly (map_poly of_int_poly ((pderiv ^^ j) g)) [:x:]) \<alpha>"
+                by (rule poly_poly_eq [symmetric])
+              also have "\<dots> = poly (poly (g' j) [:x:]) \<alpha>"
+                by (simp add: g'_def)
+              finally show ?case .
+            qed auto
+            also have "\<dots> = poly (\<Sum>x\<in>Roots q. poly (g' j) [:x:]) \<alpha>"
+              by (simp add: poly_sum)
+            also have "\<dots> = eval_poly of_rat (Q q j) \<alpha>"
+              using q by (simp add: Q eval_poly_def)
+            finally show ?case .
+          qed auto
+          also have "\<dots> = eval_poly of_rat (Q' q) \<alpha>"
+            by (simp add: Q'_def of_rat_hom.eval_poly_sum)
+          finally show ?case by simp
+        qed auto
+        finally show "J \<alpha> = - (\<Sum>q\<in>P. of_int (\<beta> q) * eval_poly of_rat (Q' q) \<alpha>)" .
+      qed
+      thus ?thesis using that[of Q'] by metis
+    qed
+
+    have "J' \<in> \<rat>"
+    proof -
+      have "(\<Prod>\<alpha>\<in>Roots q. J \<alpha>) \<in> \<rat>" if q: "q \<in> P" for q
+      proof -
+        obtain root where root: "bij_betw root {..<\<sharp>q} (Roots q)"
+          using ex_bij_betw_nat_finite[OF finite_Roots[OF q]]
+          unfolding atLeast0LessThan n_roots_def by metis
+        define Q' :: "complex poly"
+          where "Q' = -(\<Sum>q\<in>P. Polynomial.smult (of_int (\<beta> q)) (map_poly of_rat (Q q)))"
+
+        have "(\<Prod>\<alpha>\<in>Roots q. J \<alpha>) = (\<Prod>\<alpha>\<in>Roots q. -(\<Sum>q\<in>P. of_int (\<beta> q) * eval_poly of_rat (Q q) \<alpha>))"
+          by (intro prod.cong refl Q) (auto simp: Roots'_def q)
+        also have "\<dots> = (\<Prod>\<alpha>\<in>Roots q. poly Q' \<alpha>)"
+          by (simp add: Q'_def poly_sum eval_poly_def)
+        also have "\<dots> = (\<Prod>i<\<sharp>q. poly Q' (root i))"
+          by (intro prod.reindex_bij_betw [symmetric] root)
+        also have "\<dots> = insertion root (\<Prod>i<\<sharp>q. mpoly_of_poly i Q')"
+          by (simp add: insertion_prod)
+        also have "\<dots> \<in> \<rat>"
+        proof (rule symmetric_poly_of_roots_in_subring)
+          show "ring_closed (\<rat> :: complex set)"
+            by standard auto
+          then interpret Q: ring_closed "\<rat> :: complex set" .
+          show "\<forall>m. MPoly_Type.coeff (\<Prod>i<\<sharp>q. mpoly_of_poly i Q') m \<in> \<rat>"
+            by (auto intro!: Q.coeff_prod_closed sum_in_Rats
+                     simp: coeff_mpoly_of_poly when_def Q'_def Polynomial.coeff_sum)
+          show "symmetric_mpoly {..<\<sharp>q} (\<Prod>i<\<sharp>q. mpoly_of_poly i Q')"
+            by (intro symmetric_mpoly_symmetric_prod'[of _ id]) (auto simp: permutes_bij)
+          show "vars (\<Prod>i<\<sharp>q. mpoly_of_poly i Q') \<subseteq> {..<\<sharp>q}"
+            by (intro order.trans[OF vars_prod] order.trans[OF vars_mpoly_of_poly] UN_least) auto
+          define lc where "lc = (of_int (Polynomial.lead_coeff q) :: complex)"
+          have "of_int_poly q = Polynomial.smult lc (\<Prod>x\<in>Roots q. [:- x, 1:])"
+            unfolding lc_def by (rule of_int_poly_P) fact
+          also have "(\<Prod>x\<in>Roots q. [:- x, 1:]) = (\<Prod>i<\<sharp>q. [:- root i, 1:])"
+            by (intro prod.reindex_bij_betw [symmetric] root)
+          finally show "of_int_poly q = Polynomial.smult lc (\<Prod>i<\<sharp>q. [:- root i, 1:])" .
+          have "lc \<noteq> 0"
+            using q by (auto simp: lc_def)
+          thus "inverse lc * lc = 1" "inverse lc \<in> \<rat>"
+            by (auto simp: lc_def)
+        qed auto
+        finally show ?thesis .
+      qed
+      hence "(\<Prod>q\<in>P. \<Prod>\<alpha>\<in>Roots q. J \<alpha>) \<in> \<rat>"
+        by (rule prod_in_Rats)
+      also have "(\<Prod>q\<in>P. \<Prod>\<alpha>\<in>Roots q. J \<alpha>) = J'"
+        unfolding Roots'_def J'_def using disjoint
+        by (intro prod.UNION_disjoint [symmetric]) (auto simp: disjoint_family_on_def)
+      finally show "J' \<in> \<rat>" .
+    qed
+
+    text \<open>
+      Since \<open>J'\<close> is clearly an algebraic integer, we now know that it is in fact an integer.
+    \<close>
+    moreover have "algebraic_int J'"
+      unfolding J'_def 
+    proof (intro algebraic_int_prod)
+      fix x assume "x \<in> Roots'"
+      hence "fact (p - 1) alg_dvd J x"
+        by (intro J)
+      thus "algebraic_int (J x)"
+        by (rule alg_dvd_imp_algebraic_int) auto
+    qed
+    ultimately have "J' \<in> \<int>"
+      using rational_algebraic_int_is_int by blast
+
+    text \<open>
+      It is also non-zero, as none of the $J_i$ have $p$ as a factor and such cannot be zero.
+    \<close>
+    have "J' \<noteq> 0"
+      unfolding J'_def
+    proof (intro prod_nonzeroI)
+      fix \<alpha> assume "\<alpha> \<in> Roots'"
+      hence "\<not>of_nat p alg_dvd J \<alpha>"
+        using J(2)[of \<alpha>] by auto
+      thus "J \<alpha> \<noteq> 0"
+        by auto
+    qed
+
+    text \<open>
+      It then clearly follows that $(p-1)!^n \leq J$:
+    \<close>
+    have "fact (p - 1) ^ n alg_dvd J'"
+    proof -
+      have "fact (p - 1) ^ n = (\<Prod>\<alpha>\<in>Roots'. fact (p - 1))"
+        by (simp add: n_altdef)
+      also have "\<dots> alg_dvd J'"
+        unfolding J'_def by (intro prod_alg_dvd_prod J(1))
+      finally show ?thesis .
+    qed
+  
+    have "fact (p - 1) ^ n \<le> norm J'"
+    proof -
+      from \<open>J' \<in> \<int>\<close> obtain J'' where [simp]: "J' = of_int J''"
+        by (elim Ints_cases)
+      have "of_int (fact (p - 1) ^ n) = (fact (p - 1) ^ n :: complex)"
+        by simp
+      also have "\<dots> alg_dvd J'"
+        by fact
+      also have "J' = of_int J''"
+        by fact
+      finally have "fact (p - 1) ^ n dvd J''"
+        by (subst (asm) alg_dvd_of_int_iff)
+      moreover from \<open>J' \<noteq> 0\<close> have "J'' \<noteq> 0"
+        by auto
+      ultimately have "\<bar>J''\<bar> \<ge> \<bar>fact (p - 1) ^ n\<bar>"
+        by (intro dvd_imp_le_int)
+      hence "real_of_int \<bar>J''\<bar> \<ge> real_of_int \<bar>fact (p - 1) ^ n\<bar>"
+        by linarith
+      also have "real_of_int \<bar>J''\<bar> = norm J'"
+        by simp
+      finally show ?thesis
+        by simp
+    qed
+
+    text \<open>The standard M-L bound for $I_i(x)$ shows the following inequality:\<close>
+    also have "norm J' \<le> C' * C p ^ n"
+    proof -
+      have "norm J' = (\<Prod>x\<in>Roots'. norm (J x))"
+        unfolding J'_def prod_norm [symmetric] ..
+      also have "\<dots> \<le> (\<Prod>x\<in>Roots'. \<Sum>q\<in>P. real_of_int \<bar>\<beta> q\<bar> * (\<Sum>\<alpha>\<in>Roots q. cmod \<alpha> * exp (cmod \<alpha>) * C p))"
+      proof (intro prod_mono conjI)
+        fix x assume x: "x \<in> Roots'"
+        show "norm (J x) \<le> (\<Sum>q\<in>P. real_of_int \<bar>\<beta> q\<bar> * (\<Sum>\<alpha>\<in>Roots q. norm \<alpha> * exp (norm \<alpha>) * C p))"
+          unfolding J_def
+        proof (intro sum_norm_le)
+          fix q assume "q \<in> P"
+          show "norm (of_int (\<beta> q) * sum (I x) (Roots q)) \<le>
+                  real_of_int \<bar>\<beta> q\<bar> * (\<Sum>\<alpha>\<in>Roots q. norm \<alpha> * exp (norm \<alpha>) * C p)"
+            unfolding norm_mult norm_of_int of_int_abs
+          proof (intro mult_left_mono sum_norm_le)
+            fix \<alpha> assume "\<alpha> \<in> Roots q"
+            hence \<alpha>: "\<alpha> \<in> Roots'"
+              using \<open>q \<in> P\<close> by (auto simp: Roots'_def)
+            show "norm (I x \<alpha>) \<le> norm \<alpha> * exp (norm \<alpha>) * C p"
+              unfolding I_def
+            proof (intro lindemann_weierstrass_aux.lindemann_weierstrass_integral_bound)
+              fix t assume "t \<in> closed_segment 0 \<alpha>"
+              also have "closed_segment 0 \<alpha> \<subseteq> cball 0 R"
+                using \<open>R \<ge> 0\<close> R_ge[OF \<alpha>] by (intro closed_segment_subset) auto
+              finally have "norm t \<le> R" by simp
+  
+              have norm_diff_le: "norm (t - y) \<le> 2 * R" if "y \<in> Roots'" for y
+              proof -
+                have "norm (t - y) \<le> norm t + norm y"
+                  by (meson norm_triangle_ineq4)
+                also have "\<dots> \<le> R + R"
+                  by (intro add_mono[OF \<open>norm t \<le> R\<close> R_ge] that)
+                finally show ?thesis by simp
+              qed
+  
+              have "norm (poly (f_poly x) t) =
+                      \<bar>real_of_int l\<bar> ^ (n * p) * (\<Prod>y\<in>Roots'. cmod (t - y) ^ (if y = x then p - 1 else p))"
+                by (simp add: eval_f x f_def norm_mult norm_power flip: prod_norm)
+              also have "\<dots> \<le> \<bar>real_of_int l\<bar> ^ (n * p) * (\<Prod>y\<in>Roots'. (2*R) ^ (if y = x then p - 1 else p))"
+                by (intro mult_left_mono prod_mono conjI power_mono norm_diff_le) auto
+              also have "\<dots> = \<bar>real_of_int l\<bar>^(n*p) * (2^(p-1) * R^(p-1) * (2^p*R^p)^(n-1))"
+                using x by (subst prod.If_eq) (auto simp: card_Diff_subset n_altdef)
+              also have "2^(p-1) * R^(p-1) * (2^p*R^p)^(n-1) = (2^((p-1)+p*(n-1))) * (R^((p-1)+p*(n-1)))"
+                unfolding power_mult power_mult_distrib power_add by (simp add: mult_ac)
+              also have "(p-1)+p*(n-1) = p*n - 1"
+                using \<open>n > 0\<close> \<open>p > 1\<close> by (cases n) (auto simp: algebra_simps)
+              also have "2 ^ (p * n - 1) * R ^ (p * n - 1) = (2*R)^(n * p-1)"
+                unfolding power_mult_distrib by (simp add: mult_ac)
+              finally show "norm (poly (f_poly x) t) \<le> C p"
+                unfolding C_def using \<open>l > 0\<close> by simp
+            qed (use \<open>R \<ge> 0\<close> \<open>l > 0\<close> in \<open>auto simp: C_def\<close>)
+          qed auto
+        qed
+      qed auto
+      also have "\<dots> = C' * C p ^ n"
+        by (simp add: C'_def power_mult_distrib n_altdef flip: sum_distrib_right mult.assoc)
+      finally show ?thesis .
+    qed
+
+    text \<open>And with that, we have our inequality:\<close>
+    finally show "fact (p - 1) ^ n \<le> C' * C p ^ n" .
+  qed
+
+  text \<open>
+    Some simple asymptotic estimates show that this is clearly a contradiction, since
+    the left-hand side grows much faster than the right-hand side and there are infinitely many
+    sufficiently large primes:
+  \<close>
+  have freq: "frequently prime sequentially"
+    using frequently_prime_cofinite unfolding cofinite_eq_sequentially .
+  have ev: "eventually (\<lambda>p. (\<forall>q\<in>P.  int p > \<bar>\<beta> q\<bar>) \<and>
+              real p > norm (\<Prod>\<alpha>\<in>Roots'. of_int (l^n) * (\<Prod>\<alpha>'\<in>Roots'-{\<alpha>}. (\<alpha>-\<alpha>')))) sequentially"
+    by (intro eventually_ball_finite \<open>finite P\<close> ballI eventually_conj filterlim_real_sequentially
+          eventually_compose_filterlim[OF eventually_gt_at_top] filterlim_int_sequentially)
+
+  have "frequently (\<lambda>p. fact (p - 1) ^ n \<le> C' * C p ^ n) sequentially"
+    by (rule frequently_eventually_mono[OF freq ev]) (use ineq in blast)
+  moreover have "eventually (\<lambda>p. fact (p - 1) ^ n > C' * C p ^ n) sequentially"
+  proof (cases "R = 0")
+    case True
+    have "eventually (\<lambda>p. p * n > 1) at_top" using \<open>n > 0\<close>
+      by (intro eventually_compose_filterlim[OF eventually_gt_at_top] mult_nat_right_at_top)
+    thus ?thesis 
+      by eventually_elim (use \<open>n > 0\<close> True in \<open>auto simp: C_def power_0_left mult_ac\<close>)
+  next
+    case False
+    hence "R > 0"
+      using \<open>R \<ge> 0\<close> by auto
+    define D :: real where "D = (2 * R * \<bar>real_of_int l\<bar>) ^ n" 
+    have "D > 0"
+      using \<open>R > 0\<close> \<open>l > 0\<close> unfolding D_def by (intro zero_less_power) auto
+
+    have "(\<lambda>p. C' * C p ^ n) \<in> O(\<lambda>p. C p ^ n)"
+      by simp
+    also have "(\<lambda>p. C p ^ n) \<in> O(\<lambda>p. ((2 * R * l) ^ (n * p)) ^ n)"
+    proof (rule landau_o.big_power[OF bigthetaD1])
+      have np: "eventually (\<lambda>p. p * n > 0) at_top" using \<open>n > 0\<close>
+        by (intro eventually_compose_filterlim[OF eventually_gt_at_top] mult_nat_right_at_top)
+      have "eventually (\<lambda>p. (2 * R) * C p = (2 * R * l) ^ (n * p)) at_top"
+        using np
+      proof eventually_elim
+        case (elim p)
+        have "2 * R * C p = l ^ (n * p) * (2 * R) ^ (Suc (n * p - 1))"
+          by (simp add: C_def algebra_simps)
+        also have "Suc (n * p - 1) = n * p"
+          using elim by auto
+        finally show ?case
+          by (simp add: algebra_simps)
+      qed
+      hence "(\<lambda>p. (2 * R) * C p) \<in> \<Theta>(\<lambda>p. (2 * R * l) ^ (n * p))"
+        by (intro bigthetaI_cong)
+      thus "C \<in> \<Theta>(\<lambda>p. (2 * R * l) ^ (n * p))"
+        using \<open>R > 0\<close> by simp
+    qed
+    also have "\<dots> = O(\<lambda>p. (D ^ p) ^ n)"
+      using \<open>l > 0\<close> by (simp flip: power_mult add: power2_eq_square mult_ac D_def)
+    also have "(\<lambda>p. (D ^ p) ^ n) \<in> o(\<lambda>p. fact (p - 1) ^ n)"
+    proof (intro landau_o.small_power)
+      have "eventually (\<lambda>p. D ^ p = D * D ^ (p - 1)) at_top"
+        using eventually_gt_at_top[of 0]
+        by eventually_elim (use \<open>D > 0\<close> in \<open>auto simp flip: power_Suc\<close>)
+      hence "(\<lambda>p. D ^ p) \<in> \<Theta>(\<lambda>p. D * D ^ (p - 1))"
+        by (intro bigthetaI_cong)
+      hence "(\<lambda>p. D ^ p) \<in> \<Theta>(\<lambda>p. D ^ (p - 1))"
+        using \<open>D > 0\<close> by simp
+      also have "(\<lambda>p. D ^ (p - 1)) \<in> o(\<lambda>p. fact (p - 1))"
+        by (intro smalloI_tendsto[OF filterlim_compose[OF power_over_fact_tendsto_0]]
+                  filterlim_minus_nat_at_top) auto
+      finally show "(\<lambda>p. D ^ p) \<in> o(\<lambda>x. fact (x - 1))" .
+    qed fact+
+    finally have smallo: "(\<lambda>p. C' * C p ^ n) \<in> o(\<lambda>p. fact (p - 1) ^ n)" .
+    have "eventually (\<lambda>p. \<bar>C' * C p ^ n\<bar> \<le> 1/2 * fact (p - 1) ^ n) at_top"
+      using landau_o.smallD[OF smallo, of "1/2"] by simp
+    thus "eventually (\<lambda>p. C' * C p ^ n < fact (p - 1) ^ n) at_top"
+    proof eventually_elim
+      case (elim p)
+      have "C' * C p ^ n \<le> \<bar>C' * C p ^ n\<bar>"
+        by simp
+      also have "\<dots> \<le> 1/2 * fact (p - 1) ^ n"
+        by fact
+      also have "\<dots> < fact (p - 1) ^ n"
+        by simp
+      finally show ?case .
+    qed
+  qed
+  ultimately have "frequently (\<lambda>p::nat. False) sequentially"
+    by (rule frequently_eventually_mono) auto
+  thus False
+    by simp
+qed
+
+
+subsection \<open>Removing the restriction of full sets of conjugates\<close>
+
+text \<open>
+  We will now remove the restriction that the $\alpha_i$ must occur in full sets of conjugates
+  by multiplying the equality with all permutations of roots.
+\<close>
+lemma Hermite_Lindemann_aux2:
+  fixes X :: "complex set" and \<beta> :: "complex \<Rightarrow> int"
+  assumes "finite X"
+  assumes nz:   "\<And>x. x \<in> X \<Longrightarrow> \<beta> x \<noteq> 0"
+  assumes alg:  "\<And>x. x \<in> X \<Longrightarrow> algebraic x"
+  assumes sum0: "(\<Sum>x\<in>X. of_int (\<beta> x) * exp x) = 0"
+  shows   "X = {}"
+proof (rule ccontr)
+  assume "X \<noteq> {}"
+  note [intro] = \<open>finite X\<close>
+
+  text \<open>
+    Let \<open>P\<close> be the smallest integer polynomial whose roots are a superset of \<open>X\<close>:
+  \<close>
+  define P :: "int poly" where "P = \<Prod>(min_int_poly ` X)"
+  define Roots :: "complex set" where "Roots = {x. ipoly P x = 0}"
+  have [simp]: "P \<noteq> 0"
+    using \<open>finite X\<close> by (auto simp: P_def)
+  have [intro]: "finite Roots"
+    unfolding Roots_def by (intro poly_roots_finite) auto
+
+  have "X \<subseteq> Roots"
+  proof safe
+    fix x assume "x \<in> X"
+    hence "ipoly (min_int_poly x) x = 0"
+      by (intro ipoly_min_int_poly alg)
+    thus "x \<in> Roots"
+      using \<open>finite X\<close> \<open>x \<in> X\<close>
+      by (auto simp: Roots_def P_def of_int_poly_hom.hom_prod poly_prod)
+  qed
+
+  have "squarefree (of_int_poly P :: complex poly)"
+    unfolding P_def of_int_poly_hom.hom_prod
+  proof (rule squarefree_prod_coprime; safe)
+    fix x assume "x \<in> X"
+    thus "squarefree (of_int_poly (min_int_poly x) :: complex poly)"
+      by (intro squarefree_of_int_polyI) auto
+  next
+    fix x y assume xy: "x \<in> X" "y \<in> X" "min_int_poly x \<noteq> min_int_poly y"
+    thus "Rings.coprime (of_int_poly (min_int_poly x)) (of_int_poly (min_int_poly y) :: complex poly)"
+      by (intro coprime_of_int_polyI[OF primes_coprime]) auto
+  qed
+
+  text \<open>
+    Since we will need a numbering of these roots, we obtain one:
+  \<close>
+  define n where "n = card Roots"
+  obtain Root where Root: "bij_betw Root {..<n} Roots"
+    using ex_bij_betw_nat_finite[OF \<open>finite Roots\<close>] unfolding n_def atLeast0LessThan by metis
+  define unRoot :: "complex \<Rightarrow> nat" where "unRoot = inv_into {..<n} Root"
+  have unRoot: "bij_betw unRoot Roots {..<n}"
+    unfolding unRoot_def by (intro bij_betw_inv_into Root)
+  have unRoot_Root [simp]: "unRoot (Root i) = i" if "i < n" for i
+    unfolding unRoot_def using Root that by (subst inv_into_f_f) (auto simp: bij_betw_def)
+  have Root_unRoot [simp]: "Root (unRoot x) = x" if "x \<in> Roots" for x
+    unfolding unRoot_def using Root that by (subst f_inv_into_f) (auto simp: bij_betw_def)
+  have [simp, intro]: "Root i \<in> Roots" if "i < n" for i
+    using Root that by (auto simp: bij_betw_def)
+  have [simp, intro]: "unRoot x < n" if "x \<in> Roots" for x
+    using unRoot that by (auto simp: bij_betw_def)
+
+  text \<open>
+    We will also need to convert between permutations of natural numbers less than \<open>n\<close> and
+    permutations of the roots:
+  \<close>
+  define convert_perm :: "(nat \<Rightarrow> nat) \<Rightarrow> (complex \<Rightarrow> complex)" where
+    "convert_perm = (\<lambda>\<sigma> x. if x \<in> Roots then Root (\<sigma> (unRoot x)) else x)"
+  have bij_convert: "bij_betw convert_perm {\<sigma>. \<sigma> permutes {..<n}} {\<sigma>. \<sigma> permutes Roots}"
+    using bij_betw_permutations[OF Root] unfolding convert_perm_def unRoot_def .
+  have permutes_convert_perm [intro]: "convert_perm \<sigma> permutes Roots" if "\<sigma> permutes {..<n}" for \<sigma>
+    using that bij_convert unfolding bij_betw_def by blast
+  have convert_perm_compose: "convert_perm (\<pi> \<circ> \<sigma>) = convert_perm \<pi> \<circ> convert_perm \<sigma>"
+    if "\<pi> permutes {..<n}" "\<sigma> permutes {..<n}" for \<sigma> \<pi>
+  proof (intro ext)
+    fix x show "convert_perm (\<pi> \<circ> \<sigma>) x = (convert_perm \<pi> \<circ> convert_perm \<sigma>) x"
+    proof (cases "x \<in> Roots")
+      case True
+      thus ?thesis
+        using permutes_in_image[OF that(2), of "unRoot x"]
+        by (auto simp: convert_perm_def bij_betw_def)
+    qed (auto simp: convert_perm_def)
+  qed
+
+  text \<open>
+    We extend the coefficient vector to the new roots by setting their coefficients to 0:
+  \<close>
+  define \<beta>' where "\<beta>' = (\<lambda>x. if x \<in> X then \<beta> x else 0)"
+
+  text \<open>
+    We now define the set of all permutations of our roots:
+  \<close>
+  define perms where "perms = {\<pi>. \<pi> permutes Roots}"
+  have [intro]: "finite perms"
+    unfolding perms_def by (rule finite_permutations) auto
+  have [simp]: "card perms = fact n"
+    unfolding perms_def n_def by (intro card_permutations) auto
+
+  text \<open>
+    The following is the set of all \<open>n!\<close>-tuples of roots, disregarding permutation of components.
+    In other words: all multisets of roots with size \<open>n!\<close>.
+  \<close>
+  define Roots_ms :: "complex multiset set" where
+    "Roots_ms = {X. set_mset X \<subseteq> Roots \<and> size X = fact n}"
+  have [intro]: "finite Roots_ms"
+    unfolding Roots_ms_def by (rule finite_multisets_of_size) auto
+
+  text \<open>
+    Next, the following is the set of \<open>n!\<close>-tuples whose entries are precisely the multiset \<open>X\<close>:
+  \<close>
+  define tuples :: "complex multiset \<Rightarrow> ((complex \<Rightarrow> complex) \<Rightarrow> complex) set" where
+    "tuples = (\<lambda>X. {f\<in>perms \<rightarrow>\<^sub>E Roots. image_mset f (mset_set perms) = X})"
+  have fin_tuples [intro]: "finite (tuples X)" for X
+    unfolding tuples_def by (rule finite_subset[of _ "perms \<rightarrow>\<^sub>E Roots", OF _ finite_PiE]) auto
+  define tuples' :: "(complex multiset \<times> ((complex \<Rightarrow> complex) \<Rightarrow> complex)) set" where
+    "tuples' = (SIGMA X:Roots_ms. tuples X)"
+
+  text \<open>
+    The following shows that our \<^term>\<open>tuples\<close> definition is stable under permutation of
+    the roots.
+  \<close>
+  have bij_convert': "bij_betw (\<lambda>f. f \<circ> (\<lambda>g. \<sigma> \<circ> g)) (tuples X) (tuples X)"
+    if \<sigma>: "\<sigma> permutes Roots" for \<sigma> X
+  proof (rule bij_betwI)
+    have *: "(\<lambda>f. f \<circ> (\<circ>) \<sigma>) \<in> tuples X \<rightarrow> tuples X" if \<sigma>: "\<sigma> permutes Roots" for \<sigma>
+    proof
+      fix f assume f: "f \<in> tuples X"
+      show "f \<circ> (\<circ>) \<sigma> \<in> tuples X"
+        unfolding tuples_def
+      proof safe
+        fix \<sigma>'
+        assume \<sigma>': "\<sigma>' \<in> perms"
+        show "(f \<circ> (\<circ>) \<sigma>) \<sigma>' \<in> Roots"
+          using permutes_compose[OF _ \<sigma>, of \<sigma>'] \<sigma> \<sigma>' f by (auto simp: perms_def tuples_def)
+      next
+        fix \<sigma>'
+        assume \<sigma>': "\<sigma>' \<notin> perms"
+        have "\<not>(\<sigma> \<circ> \<sigma>') permutes Roots"
+        proof
+          assume "(\<sigma> \<circ> \<sigma>') permutes Roots"
+          hence "inv_into UNIV \<sigma> \<circ> (\<sigma> \<circ> \<sigma>') permutes Roots"
+            by (rule permutes_compose) (use permutes_inv[OF \<sigma>] in simp_all)
+          also have "inv_into UNIV \<sigma> \<circ> (\<sigma> \<circ> \<sigma>') = \<sigma>'"
+            by (auto simp: fun_eq_iff permutes_inverses[OF \<sigma>])
+          finally show False using \<sigma>' by (simp add: perms_def)
+        qed
+        thus "(f \<circ> (\<circ>) \<sigma>) \<sigma>' = undefined"
+          using f by (auto simp: perms_def tuples_def)
+      next
+        have "image_mset (f \<circ> (\<circ>) \<sigma>) (mset_set perms) =
+              image_mset f (image_mset ((\<circ>) \<sigma>) (mset_set perms))"
+          by (rule multiset.map_comp [symmetric])
+        also have "image_mset ((\<circ>) \<sigma>) (mset_set perms) = mset_set perms"
+          using bij_betw_permutes_compose_left[OF \<sigma>]
+          by (subst image_mset_mset_set) (auto simp: bij_betw_def perms_def)
+        also have "image_mset f \<dots> = X"
+          using f by (auto simp: tuples_def)
+        finally show "image_mset (f \<circ> (\<circ>) \<sigma>) (mset_set perms) = X" .
+      qed
+    qed
+
+    show "(\<lambda>f. f \<circ> (\<circ>) \<sigma>) \<in> tuples X \<rightarrow> tuples X"
+      by (rule *) fact
+    show "(\<lambda>f. f \<circ> (\<circ>) (inv_into UNIV \<sigma>)) \<in> tuples X \<rightarrow> tuples X"
+      by (intro * permutes_inv) fact
+    show "f \<circ> (\<circ>) \<sigma> \<circ> (\<circ>) (inv_into UNIV \<sigma>) = f" if "f \<in> tuples X" for f
+      by (auto simp: fun_eq_iff o_def permutes_inverses[OF \<sigma>])
+    show "f \<circ> (\<circ>) (inv_into UNIV \<sigma>) \<circ> (\<circ>) \<sigma> = f" if "f \<in> tuples X" for f
+      by (auto simp: fun_eq_iff o_def permutes_inverses[OF \<sigma>])
+  qed
+
+  text \<open>
+    Next, we define the multiset of of possible exponents that we can get for a given
+    \<open>n!\<close>-multiset of roots,
+  \<close>
+  define R :: "complex multiset \<Rightarrow> complex multiset" where
+    "R = (\<lambda>X. image_mset (\<lambda>f. \<Sum>\<sigma>\<in>perms. \<sigma> (f \<sigma>)) (mset_set (tuples X)))"
+
+  text \<open>
+    We show that, for each such multiset, there is a content-free integer polynomial that has
+    exactly these exponents as roots. This shows that they form a full set of conjugates (but
+    note this polynomial is not necessarily squarefree).
+
+    The proof is yet another application of the fundamental theorem of symmetric polynomials.
+  \<close>
+  obtain Q :: "complex multiset \<Rightarrow> int poly"
+    where Q: "\<And>X. X \<in> Roots_ms \<Longrightarrow> poly_roots (of_int_poly (Q X)) = R X"
+             "\<And>X. X \<in> Roots_ms \<Longrightarrow> content (Q X) = 1"
+  proof -
+    {
+      fix X :: "complex multiset"
+      assume X: "X \<in> Roots_ms"
+      define Q :: "complex poly mpoly" where
+        "Q = (\<Prod>f\<in>tuples X. Const [:0, 1:] -
+                 (\<Sum>\<sigma> | \<sigma> permutes {..<n}. Var (\<sigma> (unRoot (f (convert_perm \<sigma>))))))"
+      define Q1 where "Q1 = (\<Prod>f\<in>tuples X. [:- (\<Sum>\<sigma> | \<sigma> permutes Roots. \<sigma> (f \<sigma>)), 1:])"
+      define ratpolys :: "complex poly set" where "ratpolys = {p. \<forall>i. poly.coeff p i \<in> \<rat>}"
+
+      have "insertion (\<lambda>x. [:Root x:]) Q \<in> ratpolys"
+      proof (rule symmetric_poly_of_roots_in_subring[where l = "\<lambda>x. [:x:]"])
+        show "ring_closed ratpolys"
+          unfolding ratpolys_def by standard (auto intro: coeff_mult_semiring_closed)
+        then interpret ratpolys: ring_closed ratpolys .
+        have "pCons 0 1 \<in> ratpolys "
+          by (auto simp: ratpolys_def coeff_pCons split: nat.splits)
+        thus "\<forall>m. MPoly_Type.coeff Q m \<in> ratpolys"
+          unfolding Q_def
+          by (intro allI ratpolys.coeff_prod_closed)
+             (auto intro!: ratpolys.minus_closed ratpolys.sum_closed ratpolys.uminus_closed simp: coeff_Var mpoly_coeff_Const when_def)
+      next
+        show "ring_homomorphism (\<lambda>x::complex. [:x:])" ..
+      next
+        have "\<sigma> (unRoot (f (convert_perm \<sigma>))) < n" if "f \<in> tuples X" "\<sigma> permutes {..<n}" for f \<sigma>
+        proof -
+          have "convert_perm \<sigma> \<in> perms"
+            using bij_convert that(2) by (auto simp: bij_betw_def perms_def)
+          hence "f (convert_perm \<sigma>) \<in> Roots"
+            using that by (auto simp: tuples_def)
+          thus ?thesis
+            using permutes_in_image[OF that(2)] by simp
+        qed
+        thus "vars Q \<subseteq> {..<n}"
+          unfolding Q_def
+          by (intro order.trans[OF vars_prod] UN_least order.trans[OF vars_sum]
+                order.trans[OF vars_diff] Un_least) (auto simp: vars_Var)
+      next
+        define lc :: complex where "lc = of_int (Polynomial.lead_coeff P)"
+        show "[:inverse lc:] \<in> ratpolys"
+          by (auto simp: ratpolys_def coeff_pCons lc_def split: nat.splits)
+        show "\<forall>i. [:poly.coeff (of_int_poly P) i:] \<in> ratpolys"
+          by (auto simp: ratpolys_def coeff_pCons split: nat.splits)
+        have "lc \<noteq> 0"
+          by (auto simp: lc_def)
+        thus "[:inverse lc:] * [:lc:] = 1"
+          by auto
+        have "rsquarefree (of_int_poly P :: complex poly)"
+          using \<open>squarefree (of_int_poly P :: complex poly)\<close> by (intro squarefree_imp_rsquarefree)
+        hence "of_int_poly P = Polynomial.smult lc (\<Prod>x\<in>Roots. [:-x, 1:])"
+          unfolding lc_def Roots_def of_int_hom.hom_lead_coeff[symmetric]
+          by (rule complex_poly_decompose_rsquarefree [symmetric])
+        also have "(\<Prod>x\<in>Roots. [:-x, 1:]) = (\<Prod>i<n. [:-Root i, 1:])"
+          by (rule prod.reindex_bij_betw[OF Root, symmetric])
+        finally show "of_int_poly P = Polynomial.smult lc (\<Prod>i<n. [:- Root i, 1:])" .
+      next
+        show "symmetric_mpoly {..<n} Q"
+          unfolding symmetric_mpoly_def
+        proof safe
+          fix \<pi> assume \<pi>: "\<pi> permutes {..<n}"
+          have "mpoly_map_vars \<pi> Q = (\<Prod>f\<in>tuples X. Const (pCons 0 1) - (\<Sum> \<sigma> | \<sigma> permutes {..<n}.
+                  Var ((\<pi> \<circ> \<sigma>) (unRoot (f (convert_perm \<sigma>))))))"
+            by (simp add: Q_def permutes_bij[OF \<pi>])
+          also have "\<dots> = (\<Prod>f\<in>tuples X. Const (pCons 0 1) - (\<Sum> \<sigma> | \<sigma> permutes {..<n}.
+                  Var ((\<pi> \<circ> \<sigma>) (unRoot ((f \<circ> (\<lambda>\<sigma>. convert_perm \<pi> \<circ> \<sigma>)) (convert_perm \<sigma>))))))"
+            using \<pi> by (intro prod.reindex_bij_betw [OF bij_convert', symmetric]) auto
+          also have "\<dots> = Q"
+            unfolding Q_def
+          proof (rule prod.cong, goal_cases)
+            case (2 f)
+            have "(\<Sum> \<sigma> | \<sigma> permutes {..<n}. Var ((\<pi> \<circ> \<sigma>) (unRoot ((f \<circ> (\<lambda>\<sigma>. convert_perm \<pi> \<circ> \<sigma>)) (convert_perm \<sigma>))))) =
+                  (\<Sum> \<sigma> | \<sigma> permutes {..<n}. Var ((\<pi> \<circ> \<sigma>) (unRoot (f (convert_perm (\<pi> \<circ> \<sigma>))))))"
+              using \<pi> by (intro sum.cong refl, subst convert_perm_compose) simp_all
+            also have "\<dots> = (\<Sum> \<sigma> | \<sigma> permutes {..<n}. Var (\<sigma> (unRoot (f (convert_perm \<sigma>)))))"
+              using \<pi> by (rule setum_permutations_compose_left [symmetric])
+            finally show ?case by simp
+          qed auto
+          finally show "mpoly_map_vars \<pi> Q = Q" .
+        qed
+      qed auto
+      also have "insertion (\<lambda>x. [:Root x:]) Q = Q1"
+        unfolding Q_def Q1_def insertion_prod insertion_sum insertion_diff insertion_Const insertion_Var
+      proof (intro prod.cong, goal_cases)
+        case f: (2 f)
+        have "(\<Sum>\<sigma> | \<sigma> permutes {..<n}. [:Root (\<sigma> (unRoot (f (convert_perm \<sigma>)))):]) =
+              (\<Sum>\<sigma> | \<sigma> permutes {..<n}. [:convert_perm \<sigma> (f (convert_perm \<sigma>)):])"
+        proof (rule sum.cong, goal_cases)
+          case (2 \<sigma>)
+          have "convert_perm \<sigma> permutes Roots"
+            using bij_convert 2 by (auto simp: bij_betw_def)
+          hence "f (convert_perm \<sigma>) \<in> Roots"
+            using f by (auto simp: tuples_def perms_def)
+          thus ?case by (simp add: convert_perm_def)
+        qed simp_all
+        also have "\<dots> = (\<Sum>\<sigma> | \<sigma> permutes Roots. [:\<sigma> (f \<sigma>):])"
+          by (rule sum.reindex_bij_betw[OF bij_convert])
+        finally show ?case
+          by (simp flip: pCons_one coeff_lift_hom.hom_sum)
+      qed simp_all
+      finally have "Q1 \<in> ratpolys"
+        by auto
+      then obtain Q2 :: "rat poly" where Q2: "Q1 = map_poly of_rat Q2"
+        unfolding ratpolys_def using ratpolyE[of Q1] by blast
+
+      have "Q1 \<noteq> 0"
+        unfolding Q1_def using fin_tuples[of X] by auto
+      with Q2 have "Q2 \<noteq> 0"
+        by auto
+      obtain Q3 :: "int poly" and lc :: rat
+        where Q3: "Q2 = Polynomial.smult lc (of_int_poly Q3)" and "lc > 0" and "content Q3 = 1"
+        using rat_to_normalized_int_poly_exists[OF \<open>Q2 \<noteq> 0\<close>] by metis
+
+      have "poly_roots (of_int_poly Q3) = poly_roots (map_poly (of_rat \<circ> of_int) Q3)"
+        by simp
+      also have "map_poly (of_rat \<circ> of_int) Q3 = map_poly of_rat (map_poly of_int Q3)"
+        by (subst map_poly_map_poly) auto
+      also have "poly_roots \<dots> = poly_roots (Polynomial.smult (of_rat lc) \<dots>)"
+        using \<open>lc > 0\<close> by simp
+      also have "Polynomial.smult (of_rat lc) (map_poly of_rat (map_poly of_int Q3)) =
+                 map_poly of_rat (Polynomial.smult lc (map_poly of_int Q3))"
+        by (simp add: of_rat_hom.map_poly_hom_smult)
+      also have "\<dots> = Q1"
+        by (simp only: Q3 [symmetric] Q2 [symmetric])
+      also have "poly_roots Q1 = R X"
+        unfolding Q1_def
+        by (subst poly_roots_prod, force, subst poly_roots_linear)
+           (auto simp: R_def perms_def sum_mset_image_mset_singleton sum_unfold_sum_mset)
+      finally have "\<exists>Q. poly_roots (of_int_poly Q) = R X \<and> content Q = 1"
+        using \<open>content Q3 = 1\<close> by metis
+    }
+    hence "\<exists>Q. \<forall>X\<in>Roots_ms. poly_roots (of_int_poly (Q X)) = R X \<and> content (Q X) = 1"
+      by metis
+    thus ?thesis using that by metis
+  qed
+
+  text \<open>
+    We can now collect all the $e^{\sum \alpha_i}$ that happen to be equal and let the following
+    be their coefficients:
+  \<close>
+  define \<beta>'' :: "int poly \<Rightarrow> int"
+    where "\<beta>'' = (\<lambda>q. \<Sum>X\<in>Roots_ms. int (count (prime_factorization (Q X)) q) * (\<Prod>x\<in>#X. \<beta>' x))"
+  have supp_\<beta>'': "{q. \<beta>'' q \<noteq> 0} \<subseteq> (\<Union>X\<in>Roots_ms. prime_factors (Q X))"
+    unfolding \<beta>''_def using sum.not_neutral_contains_not_neutral by fastforce
+
+  text \<open>
+    We have to prove that \<open>\<beta>''\<close> is not zero everywhere. We do this by selecting the nonzero term
+    with the maximal exponent (w.r.t. the lexicographic ordering on the complex numbers) in every
+    factor of the product and show that there is no other summand corresponding to these, so
+    that their non-zero coefficient cannot get cancelled.
+  \<close>
+  have "{q. \<beta>'' q \<noteq> 0} \<noteq> {}"
+  proof -
+    define f where "f = restrict (\<lambda>\<sigma>. inv_into UNIV \<sigma> (complex_lex.Max (\<sigma> ` X))) perms"
+    have f: "f \<in> perms \<rightarrow> X"
+    proof
+      fix \<sigma> assume \<sigma>: "\<sigma> \<in> perms"
+      have "complex_lex.Max (\<sigma> ` X) \<in> \<sigma> ` X"
+        using \<open>X \<noteq> {}\<close> by (intro complex_lex.Max_in finite_imageI) auto
+      thus "f \<sigma> \<in> X"
+        using \<sigma> by (auto simp: f_def permutes_inverses[of \<sigma> Roots] perms_def)
+    qed
+    hence f': "f \<in> perms \<rightarrow>\<^sub>E Roots"
+      using \<open>X \<subseteq> Roots\<close> by (auto simp: f_def PiE_def)
+
+    define Y where "Y = image_mset f (mset_set perms)"
+    have "Y \<in> Roots_ms" using f' \<open>finite perms\<close>
+      by (auto simp: Roots_ms_def Y_def)
+
+    have "(\<Sum>\<sigma>\<in>perms. \<sigma> (f \<sigma>)) \<in># R Y"
+    proof -
+      from f' have "f \<in> tuples Y"
+        unfolding tuples_def Y_def by simp
+      thus ?thesis
+        unfolding R_def using fin_tuples[of Y] by auto
+    qed
+    also have "R Y = poly_roots (of_int_poly (Q Y))"
+      by (rule Q(1) [symmetric]) fact
+    also have "\<dots> = (\<Sum>p\<in>#prime_factorization (Q Y). poly_roots (of_int_poly p))"
+      by (rule poly_roots_of_int_conv_sum_prime_factors)
+    finally obtain q where q: "q \<in> prime_factors (Q Y)" "(\<Sum>\<sigma>\<in>perms. \<sigma> (f \<sigma>)) \<in># poly_roots (of_int_poly q)"
+      by auto
+
+    have "\<beta>'' q = (\<Sum>X\<in>{Y}. int (count (prime_factorization (Q X)) q) * prod_mset (image_mset \<beta>' X))"
+      unfolding \<beta>''_def
+    proof (intro sum.mono_neutral_right ballI)
+      fix Y' assume Y': "Y' \<in> Roots_ms - {Y}"
+      show "int (count (prime_factorization (Q Y')) q) * \<Prod>\<^sub># (image_mset \<beta>' Y') = 0"
+      proof (cases "set_mset Y' \<subseteq> X")
+        case Y'_subset: True
+        have "q \<notin> prime_factors (Q Y')"
+        proof
+          assume q': "q \<in> prime_factors (Q Y')"
+          have "poly_roots (of_int_poly q :: complex poly) \<subseteq>#
+                         poly_roots (of_int_poly (Q Y'))"
+            using q' by (intro dvd_imp_poly_roots_subset of_int_poly_hom.hom_dvd) auto
+          with q(2) have "(\<Sum>\<sigma>\<in>perms. \<sigma> (f \<sigma>)) \<in># poly_roots (of_int_poly (Q Y'))"
+            by (meson mset_subset_eqD)
+          also have "poly_roots (of_int_poly (Q Y')) = R Y'"
+            using Q(1)[of Y'] Y' by auto
+          finally obtain g where g: "g \<in> tuples Y'" "(\<Sum>\<sigma>\<in>perms. \<sigma> (f \<sigma>)) = (\<Sum>\<sigma>\<in>perms. \<sigma> (g \<sigma>))"
+            unfolding R_def using fin_tuples[of Y'] by auto
+
+          moreover have "(\<Sum>\<sigma>\<in>perms. \<sigma> (g \<sigma>)) <\<^sub>\<complex> (\<Sum>\<sigma>\<in>perms. \<sigma> (f \<sigma>))"
+          proof (rule sum_strict_mono_ex1_complex_lex)
+            show le: "\<forall>\<sigma>\<in>perms. \<sigma> (g \<sigma>) \<le>\<^sub>\<complex> \<sigma> (f \<sigma>)"
+            proof
+              fix \<sigma> assume \<sigma>: "\<sigma> \<in> perms"
+              hence \<sigma>': "\<sigma> permutes Roots"
+                by (auto simp: perms_def)
+              have "image_mset g (mset_set perms) = Y'"
+                using g by (auto simp: tuples_def)
+              also have "set_mset \<dots> \<subseteq> X"
+                by fact
+              finally have "g ` perms \<subseteq> X"
+                using \<open>finite perms\<close> by auto
+              hence "\<sigma> (g \<sigma>) \<le>\<^sub>\<complex> complex_lex.Max (\<sigma> ` X)"
+                using \<open>finite perms\<close> \<sigma>
+                by (intro complex_lex.Max.coboundedI finite_imageI imageI)
+                   (auto simp: tuples_def)
+              also have "\<dots> = \<sigma> (f \<sigma>)"
+                using \<sigma> by (simp add: f_def permutes_inverses[OF \<sigma>'])
+              finally show "\<sigma> (g \<sigma>) \<le>\<^sub>\<complex> \<sigma> (f \<sigma>)" .
+            qed
+
+            have "image_mset g (mset_set perms) \<noteq> image_mset f (mset_set perms)"
+              using Y' g by (auto simp: tuples_def Y_def)
+            then obtain \<sigma> where \<sigma>: "\<sigma> \<in># mset_set perms" "g \<sigma> \<noteq> f \<sigma>"
+              by (meson multiset.map_cong)
+            have "\<sigma> permutes Roots"
+              using \<sigma> \<open>finite perms\<close> by (auto simp: perms_def)
+            have "\<sigma> (g \<sigma>) \<noteq> \<sigma> (f \<sigma>)"
+              using permutes_inj[OF \<open>\<sigma> permutes Roots\<close>] \<sigma> by (auto simp: inj_def)
+            moreover have "\<sigma> (g \<sigma>) \<le>\<^sub>\<complex> \<sigma> (f \<sigma>)"
+              using le \<sigma> \<open>finite perms\<close> by auto
+            ultimately have "\<sigma> (g \<sigma>) <\<^sub>\<complex> \<sigma> (f \<sigma>)"
+              by simp
+            thus "\<exists>\<sigma>\<in>perms. \<sigma> (g \<sigma>) <\<^sub>\<complex> \<sigma> (f \<sigma>)"
+              using \<sigma> \<open>finite perms\<close> by auto
+          qed (use \<open>finite perms\<close> in simp_all)
+          ultimately show False by simp
+        qed
+        thus ?thesis by auto
+      qed (auto simp: \<beta>'_def)
+    qed (use \<open>Y \<in> Roots_ms\<close> in auto)
+    also have "\<dots> = int (count (prime_factorization (Q Y)) q) * prod_mset (image_mset \<beta>' Y)"
+      by simp
+    also have "\<dots> \<noteq> 0"
+      using q nz \<open>finite X\<close> \<open>X \<noteq> {}\<close> \<open>finite perms\<close> f by (auto simp: \<beta>'_def Y_def)
+    finally show "{q. \<beta>'' q \<noteq> 0} \<noteq> {}"
+      by auto
+  qed
+
+  text \<open>
+    We are now ready for the final push: we start with the original sum that we know to be zero,
+    multiply it with the other permutations, and then multiply out the sum.
+  \<close>
+  have "0 = (\<Sum>x\<in>X. \<beta> x * exp x)"
+    using sum0 ..
+  also have "\<dots> = (\<Sum>x\<in>Roots. \<beta>' x * exp x)"
+    by (intro sum.mono_neutral_cong_left \<open>X \<subseteq> Roots\<close>) (auto simp: \<beta>'_def)
+  also have "\<dots> dvd (\<Prod>\<sigma>\<in>perms. \<Sum>x\<in>Roots. \<beta>' x * exp (\<sigma> x))"
+    by (rule dvd_prodI[OF \<open>finite perms\<close>])
+       (use permutes_id[of Roots] in \<open>simp_all add: id_def perms_def\<close>)
+  also have "\<dots> = (\<Sum>f\<in>perms \<rightarrow>\<^sub>E Roots. \<Prod>\<sigma>\<in>perms. \<beta>' (f \<sigma>) * exp (\<sigma> (f \<sigma>)))"
+    by (rule prod_sum_PiE) auto
+  also have "\<dots> = (\<Sum>f\<in>perms \<rightarrow>\<^sub>E Roots. (\<Prod>\<sigma>\<in>perms. \<beta>' (f \<sigma>)) * exp (\<Sum>\<sigma>\<in>perms. \<sigma> (f \<sigma>)))"
+    using \<open>finite perms\<close> by (simp add: prod.distrib exp_sum)
+  also have "\<dots> = (\<Sum>(X,f)\<in>tuples'. (\<Prod>\<sigma>\<in>perms. \<beta>' (f \<sigma>)) * exp (\<Sum>\<sigma>\<in>perms. \<sigma> (f \<sigma>)))"
+    using \<open>finite perms\<close>
+    by (intro sum.reindex_bij_witness[of _ snd "\<lambda>f. (image_mset f (mset_set perms), f)"])
+       (auto simp: tuples'_def tuples_def Roots_ms_def PiE_def Pi_def)
+  also have "\<dots> = (\<Sum>(X,f)\<in>tuples'. (\<Prod>x\<in>#X. \<beta>' x) * exp (\<Sum>\<sigma>\<in>perms. \<sigma> (f \<sigma>)))"
+  proof (safe intro!: sum.cong)
+    fix X :: "complex multiset" and f :: "(complex \<Rightarrow> complex) \<Rightarrow> complex"
+    assume "(X, f) \<in> tuples'"
+    hence X: "X \<in> Roots_ms" "X = image_mset f (mset_set perms)" and f: "f \<in> perms \<rightarrow>\<^sub>E Roots"
+      by (auto simp: tuples'_def tuples_def)
+    have "(\<Prod>\<sigma>\<in>perms. \<beta>' (f \<sigma>)) = (\<Prod>\<sigma>\<in>#mset_set perms. \<beta>' (f \<sigma>))"
+      by (meson prod_unfold_prod_mset)
+    also have "\<dots> = (\<Prod>x\<in>#X. \<beta>' x)"
+      unfolding X(2) by (simp add: multiset.map_comp o_def)
+    finally show "(\<Prod>\<sigma>\<in>perms. \<beta>' (f \<sigma>)) * exp (\<Sum>\<sigma>\<in>perms. \<sigma> (f \<sigma>)) =
+                  (\<Prod>x\<in>#X. \<beta>' x) * exp (\<Sum>\<sigma>\<in>perms. \<sigma> (f \<sigma>))" by simp
+  qed
+  also have "\<dots> = (\<Sum>X\<in>Roots_ms. \<Sum>f\<in>tuples X. (\<Prod>x\<in>#X. \<beta>' x) * exp (\<Sum>\<sigma>\<in>perms. \<sigma> (f \<sigma>)))"
+    unfolding tuples'_def by (intro sum.Sigma [symmetric]) auto
+  also have "\<dots> = (\<Sum>X\<in>Roots_ms. of_int (\<Prod>x\<in>#X. \<beta>' x) * (\<Sum>f\<in>tuples X. exp (\<Sum>\<sigma>\<in>perms. \<sigma> (f \<sigma>))))"
+    by (simp add: sum_distrib_left)
+  also have "\<dots> = (\<Sum>X\<in>Roots_ms. of_int (\<Prod>x\<in>#X. \<beta>' x) * (\<Sum>x\<in>#R X. exp x))"
+    by (simp only: R_def multiset.map_comp o_def sum_unfold_sum_mset)
+  also have "\<dots> = (\<Sum>X\<in>Roots_ms. of_int (\<Prod>x\<in>#X. \<beta>' x) * (\<Sum>x\<in>#poly_roots (of_int_poly (Q X)). exp x))"
+    by (intro sum.cong) (simp_all flip: Q)
+
+  text \<open>
+    Our problem now is that the polynomials \<open>Q X\<close> can still contain multiple roots and that their
+    roots might not be disjoint. We therefore split them all into irreducible factors and collect
+    equal terms.
+  \<close>
+  also have "\<dots> = (\<Sum>X\<in>Roots_ms. (\<Sum>p. of_int (int (count (prime_factorization (Q X)) p) *
+                      (\<Prod>x\<in>#X. \<beta>' x)) * (\<Sum>x | ipoly p x = 0. exp x)))"
+  proof (rule sum.cong, goal_cases)
+    case (2 X)
+    have "(\<Sum>x\<in>#poly_roots (of_int_poly (Q X) :: complex poly). exp x) =
+          (\<Sum>x \<in># (\<Sum>p\<in>#prime_factorization (Q X). poly_roots (of_int_poly p)). exp x)"
+      by (subst poly_roots_of_int_conv_sum_prime_factors) (rule refl)
+    also have "\<dots> = (\<Sum>p\<in>#prime_factorization (Q X). \<Sum>x\<in>#poly_roots (of_int_poly p). exp x)"
+      by (rule sum_mset_image_mset_sum_mset_image_mset)
+    also have "rsquarefree (of_int_poly p :: complex poly)" if "p \<in> prime_factors (Q X)" for p
+    proof (rule irreducible_imp_rsquarefree_of_int_poly)
+      have "prime p"
+        using that by auto
+      thus "irreducible p"
+        by blast
+    next
+      show "Polynomial.degree p > 0"
+        by (intro content_1_imp_nonconstant_prime_factors[OF Q(2) that] 2)
+    qed
+    hence "(\<Sum>p\<in>#prime_factorization (Q X). \<Sum>x\<in>#poly_roots (of_int_poly p). exp x) =
+           (\<Sum>p\<in>#prime_factorization (Q X). \<Sum>x | ipoly p x = 0. exp (x :: complex))"
+      unfolding sum_unfold_sum_mset
+      by (intro arg_cong[of _ _ sum_mset] image_mset_cong sum.cong refl,
+          subst rsquarefree_poly_roots_eq) auto
+    also have "\<dots> = (\<Sum>p. count (prime_factorization (Q X)) p * (\<Sum>x | ipoly p x = 0. exp (x :: complex)))"
+      by (rule sum_mset_conv_Sum_any)
+    also have "of_int (\<Prod>x\<in>#X. \<beta>' x) * \<dots> =
+               (\<Sum>p. of_int (int (count (prime_factorization (Q X)) p) * (\<Prod>x\<in>#X. \<beta>' x)) * (\<Sum>x | ipoly p x = 0. exp x))"
+      by (subst Sum_any_right_distrib) (auto simp: mult_ac)
+    finally show ?case by simp
+  qed auto
+  also have "\<dots> = (\<Sum>q. of_int (\<beta>'' q) * (\<Sum>x | ipoly q x = 0. exp x))"
+    unfolding \<beta>''_def of_int_sum
+    by (subst Sum_any_sum_swap [symmetric]) (auto simp: sum_distrib_right)
+  also have "\<dots> = (\<Sum>q | \<beta>'' q \<noteq> 0. of_int (\<beta>'' q) * (\<Sum>x | ipoly q x = 0. exp x))"
+    by (intro Sum_any.expand_superset finite_subset[OF supp_\<beta>'']) auto
+  finally have "(\<Sum>q | \<beta>'' q \<noteq> 0. of_int (\<beta>'' q) * (\<Sum>x | ipoly q x = 0. exp (x :: complex))) = 0"
+    by simp
+
+  text \<open>
+    We are now in the situation of our the specialised Hermite--Lindemann Theorem we proved
+    earlier and can easily derive a contradiction.
+  \<close>
+  moreover have "(\<Sum>q | \<beta>'' q \<noteq> 0. of_int (\<beta>'' q) * (\<Sum>x | ipoly q x = 0. exp (x :: complex))) \<noteq> 0"
+  proof (rule Hermite_Lindemann_aux1)
+    show "finite {q. \<beta>'' q \<noteq> 0}"
+      by (rule finite_subset[OF supp_\<beta>'']) auto
+  next
+    show "pairwise Rings.coprime {q. \<beta>'' q \<noteq> 0}"
+    proof (rule pairwiseI, clarify)
+      fix p q assume pq: "p \<noteq> q" "\<beta>'' p \<noteq> 0" "\<beta>'' q \<noteq> 0"
+      hence "prime p" "prime q"
+        using supp_\<beta>'' Q(2) by auto
+      with pq show "Rings.coprime p q"
+        by (simp add: primes_coprime)
+    qed
+  next
+    fix q :: "int poly"
+    assume q: "q \<in> {q. \<beta>'' q \<noteq> 0}"
+    also note supp_\<beta>''
+    finally obtain X where X: "X \<in> Roots_ms" "q \<in> prime_factors (Q X)"
+      by blast
+    show "irreducible q"
+      using X by (intro prime_elem_imp_irreducible prime_imp_prime_elem) auto
+    show "Polynomial.degree q > 0" using X
+      by (intro content_1_imp_nonconstant_prime_factors[OF Q(2)[of X]])
+  qed (use \<open>{x. \<beta>'' x \<noteq> 0} \<noteq> {}\<close> in auto)
+
+  ultimately show False by contradiction
+qed
+
+
+subsection \<open>Removing the restriction to integer coefficients\<close>
+
+text \<open>
+  Next, we weaken the restriction that the $\beta_i$ must be integers to the restriction
+  that they must be rationals. This is done simply by multiplying with the least common multiple
+  of the demoninators.
+\<close>
+lemma Hermite_Lindemann_aux3:
+  fixes X :: "complex set" and \<beta> :: "complex \<Rightarrow> rat"
+  assumes "finite X"
+  assumes nz:   "\<And>x. x \<in> X \<Longrightarrow> \<beta> x \<noteq> 0"
+  assumes alg:  "\<And>x. x \<in> X \<Longrightarrow> algebraic x"
+  assumes sum0: "(\<Sum>x\<in>X. of_rat (\<beta> x) * exp x) = 0"
+  shows   "X = {}"
+proof -
+  define l :: int where "l = Lcm ((snd \<circ> quotient_of \<circ> \<beta>) ` X)"
+  have [simp]: "snd (quotient_of r) \<noteq> 0" for r
+    using quotient_of_denom_pos'[of r] by simp
+  have [simp]: "l \<noteq> 0"
+    using \<open>finite X\<close> by (auto simp: l_def Lcm_0_iff)
+
+  have "of_int l * \<beta> x \<in> \<int>" if "x \<in> X" for x
+  proof -
+    define a b where "a = fst (quotient_of (\<beta> x))" and "b = snd (quotient_of (\<beta> x))"
+    have "b > 0"
+      using quotient_of_denom_pos'[of "\<beta> x"] by (auto simp: b_def)
+    have "\<beta> x = of_int a / of_int b"
+      by (intro quotient_of_div) (auto simp: a_def b_def)
+    also have "of_int l * \<dots> = of_int (l * a) / of_int b"
+      using \<open>b > 0\<close> by (simp add: field_simps)
+    also have "\<dots> \<in> \<int>" using that
+      by (intro of_int_divide_in_Ints) (auto simp: l_def b_def)
+    finally show ?thesis .
+  qed
+  hence "\<forall>x\<in>X. \<exists>n. of_int n = of_int l * \<beta> x"
+    using Ints_cases by metis
+  then obtain \<beta>' where \<beta>': "of_int (\<beta>' x) = of_int l * \<beta> x" if "x \<in> X" for x
+    by metis
+
+  show ?thesis
+  proof (rule Hermite_Lindemann_aux2)
+    have "0 = of_int l * (\<Sum>x\<in>X. of_rat (\<beta> x) * exp x :: complex)"
+      by (simp add: sum0)
+    also have "\<dots> = (\<Sum>x\<in>X. of_int (\<beta>' x) * exp x)"
+      unfolding sum_distrib_left
+    proof (rule sum.cong, goal_cases)
+      case (2 x)
+      have "of_int l * of_rat (\<beta> x) = of_rat (of_int l * \<beta> x)"
+        by (simp add: of_rat_mult)
+      also have "of_int l * \<beta> x = of_int (\<beta>' x)"
+        using 2 by (rule \<beta>' [symmetric])
+      finally show ?case by (simp add: mult_ac)
+    qed simp_all
+    finally show "\<dots> = 0" ..
+  next
+    fix x assume "x \<in> X"
+    hence "of_int (\<beta>' x) \<noteq> (0 :: rat)" using nz
+      by (subst \<beta>') auto
+    thus "\<beta>' x \<noteq> 0"
+      by auto
+  qed (use alg \<open>finite X\<close> in auto)
+qed
+
+text \<open>
+  Next, we weaken the restriction that the $\beta_i$ must be rational to them being algebraic.
+  Similarly to before, this is done by multiplying over all possible permutations of the $\beta_i$
+  (in some sense) to introduce more symmetry, from which it then follows by the fundamental theorem
+  of symmetric polynomials that the resulting coefficients are rational.
+\<close>
+lemma Hermite_Lindemann_aux4:
+  fixes \<beta> :: "complex \<Rightarrow> complex"
+  assumes [intro]: "finite X"
+  assumes alg1: "\<And>x. x \<in> X \<Longrightarrow> algebraic x"
+  assumes alg2: "\<And>x. x \<in> X \<Longrightarrow> algebraic (\<beta> x)"
+  assumes nz:   "\<And>x. x \<in> X \<Longrightarrow> \<beta> x \<noteq> 0"
+  assumes sum0: "(\<Sum>x\<in>X. \<beta> x * exp x) = 0"
+  shows   "X = {}"
+proof (rule ccontr)
+  assume X: "X \<noteq> {}"
+  note [intro!] = finite_PiE
+
+  text \<open>
+    We now take more or less the same approach as before, except that now we find a polynomial
+    that has all of the conjugates of the coefficients \<open>\<beta>\<close> as roots. Note that this is a slight
+    deviation from Baker's proof, who picks one polynomial for each \<open>\<beta>\<close> independently. I did it
+    this way because, as Bernard~\cite{bernard} observed, it makes the proof a bit easier.
+  \<close>
+  define P :: "int poly" where "P = \<Prod>((min_int_poly \<circ> \<beta>) ` X)"
+  define Roots :: "complex set" where "Roots = {x. ipoly P x = 0}"
+  have "0 \<notin> Roots" using \<open>finite X\<close> alg2 nz
+    by (auto simp: Roots_def P_def poly_prod)
+  have [simp]: "P \<noteq> 0"
+    using \<open>finite X\<close> by (auto simp: P_def)
+  have [intro]: "finite Roots"
+    unfolding Roots_def by (intro poly_roots_finite) auto
+
+  have "\<beta> ` X \<subseteq> Roots"
+  proof safe
+    fix x assume "x \<in> X"
+    hence "ipoly (min_int_poly (\<beta> x)) (\<beta> x) = 0"
+      by (intro ipoly_min_int_poly alg2)
+    thus "\<beta> x \<in> Roots"
+      using \<open>finite X\<close> \<open>x \<in> X\<close>
+      by (auto simp: Roots_def P_def of_int_poly_hom.hom_prod poly_prod)
+  qed
+
+  have "squarefree (of_int_poly P :: complex poly)"
+    unfolding P_def of_int_poly_hom.hom_prod o_def
+  proof (rule squarefree_prod_coprime; safe)
+    fix x assume "x \<in> X"
+    thus "squarefree (of_int_poly (min_int_poly (\<beta> x)) :: complex poly)"
+      by (intro squarefree_of_int_polyI) auto
+  next
+    fix x y assume xy: "x \<in> X" "y \<in> X" "min_int_poly (\<beta> x) \<noteq> min_int_poly (\<beta> y)"
+    thus "Rings.coprime (of_int_poly (min_int_poly (\<beta> x)))
+            (of_int_poly (min_int_poly (\<beta> y)) :: complex poly)"
+      by (intro coprime_of_int_polyI[OF primes_coprime]) auto
+  qed
+
+  define n where "n = card Roots"
+  define m where "m = card X"
+  have "Roots \<noteq> {}"
+    using \<open>\<beta> ` X \<subseteq> Roots\<close> \<open>X \<noteq> {}\<close> by auto
+  hence "n > 0" "m > 0"
+    using \<open>finite Roots\<close> \<open>finite X\<close> \<open>X \<noteq> {}\<close> by (auto simp: n_def m_def)
+  have fin1 [simp]: "finite (X \<rightarrow>\<^sub>E Roots)"
+    by auto
+  have [simp]: "card (X \<rightarrow>\<^sub>E Roots) = n ^ m"
+    by (subst card_PiE) (auto simp: m_def n_def)
+
+  text \<open>
+    We again find a bijection between the roots and the natural numbers less than \<open>n\<close>:
+  \<close>
+  obtain Root where Root: "bij_betw Root {..<n} Roots"
+    using ex_bij_betw_nat_finite[OF \<open>finite Roots\<close>] unfolding n_def atLeast0LessThan by metis
+  define unRoot :: "complex \<Rightarrow> nat" where "unRoot = inv_into {..<n} Root"
+  have unRoot: "bij_betw unRoot Roots {..<n}"
+    unfolding unRoot_def by (intro bij_betw_inv_into Root)
+  have unRoot_Root [simp]: "unRoot (Root i) = i" if "i < n" for i
+    unfolding unRoot_def using Root that by (subst inv_into_f_f) (auto simp: bij_betw_def)
+  have Root_unRoot [simp]: "Root (unRoot x) = x" if "x \<in> Roots" for x
+    unfolding unRoot_def using Root that by (subst f_inv_into_f) (auto simp: bij_betw_def)
+  have [simp, intro]: "Root i \<in> Roots" if "i < n" for i
+    using Root that by (auto simp: bij_betw_def)
+  have [simp, intro]: "unRoot x < n" if "x \<in> Roots" for x
+    using unRoot that by (auto simp: bij_betw_def)
+
+  text \<open>
+    And we again define the set of multisets and tuples that we will get in the expanded product.
+  \<close>
+  define Roots_ms :: "complex multiset set" where
+    "Roots_ms = {Y. set_mset Y \<subseteq> X \<and> size Y = n ^ m}"
+  have [intro]: "finite Roots_ms"
+    unfolding Roots_ms_def by (rule finite_multisets_of_size) auto
+  define tuples :: "complex multiset \<Rightarrow> ((complex \<Rightarrow> complex) \<Rightarrow> complex) set"
+    where "tuples = (\<lambda>Y. {f\<in>(X \<rightarrow>\<^sub>E Roots) \<rightarrow>\<^sub>E X. image_mset f (mset_set (X \<rightarrow>\<^sub>E Roots)) = Y})"
+  have [intro]: "finite (tuples Y)" for Y
+    unfolding tuples_def by (rule finite_subset[of _ "(X \<rightarrow>\<^sub>E Roots) \<rightarrow>\<^sub>E X"]) auto
+
+  text \<open>
+    We will also need to convert permutations over the natural and over the roots again.
+  \<close>
+  define convert_perm :: "(nat \<Rightarrow> nat) \<Rightarrow> (complex \<Rightarrow> complex)" where
+    "convert_perm = (\<lambda>\<sigma> x. if x \<in> Roots then Root (\<sigma> (unRoot x)) else x)"
+  have bij_convert: "bij_betw convert_perm {\<sigma>. \<sigma> permutes {..<n}} {\<sigma>. \<sigma> permutes Roots}"
+    using bij_betw_permutations[OF Root] unfolding convert_perm_def unRoot_def .
+  have permutes_convert_perm [intro]: "convert_perm \<sigma> permutes Roots" if "\<sigma> permutes {..<n}" for \<sigma>
+    using that bij_convert unfolding bij_betw_def by blast
+
+  text \<open>
+    We also need a small lemma showing that our tuples are stable under permutation of the roots.
+  \<close>
+  have bij_betw_compose_perm: 
+    "bij_betw (\<lambda>f. restrict (\<lambda>g. f (restrict (\<pi> \<circ> g) X)) (X \<rightarrow>\<^sub>E Roots)) (tuples Y) (tuples Y)"
+    if \<pi>: "\<pi> permutes Roots" and "Y \<in> Roots_ms" for \<pi> Y
+  proof (rule bij_betwI)
+    have *: "(\<lambda>f. restrict (\<lambda>g. f (restrict (\<pi> \<circ> g) X)) (X \<rightarrow>\<^sub>E Roots)) \<in> tuples Y \<rightarrow> tuples Y"
+      if \<pi>: "\<pi> permutes Roots" for \<pi>
+    proof
+      fix f assume f: "f \<in> tuples Y"
+      hence f': "f \<in> (X \<rightarrow>\<^sub>E Roots) \<rightarrow>\<^sub>E X"
+        by (auto simp: tuples_def)
+      define f' where "f' = (\<lambda>g. f (restrict (\<pi> \<circ> g) X))"
+      have "f' \<in> (X \<rightarrow>\<^sub>E Roots) \<rightarrow> X" unfolding f'_def
+        using f' bij_betw_apply[OF bij_betw_compose_left_perm_PiE[OF \<pi>, of X]] by blast
+      hence "restrict f' (X \<rightarrow>\<^sub>E Roots) \<in> (X \<rightarrow>\<^sub>E Roots) \<rightarrow>\<^sub>E X"
+        by simp
+      moreover have "image_mset (restrict f' (X \<rightarrow>\<^sub>E Roots)) (mset_set (X \<rightarrow>\<^sub>E Roots)) = Y"
+      proof -
+        have "image_mset (restrict f' (X \<rightarrow>\<^sub>E Roots)) (mset_set (X \<rightarrow>\<^sub>E Roots)) =
+              image_mset f' (mset_set (X \<rightarrow>\<^sub>E Roots))"
+          by (intro image_mset_cong) auto
+        also have "\<dots> = image_mset f (image_mset (\<lambda>g. restrict (\<pi> \<circ> g) X) (mset_set (X \<rightarrow>\<^sub>E Roots)))"
+          unfolding f'_def o_def multiset.map_comp by (simp add: o_def)
+        also have "image_mset (\<lambda>g. restrict (\<pi> \<circ> g) X) (mset_set (X \<rightarrow>\<^sub>E Roots)) =
+                   mset_set (X \<rightarrow>\<^sub>E Roots)"
+          by (intro bij_betw_image_mset_set bij_betw_compose_left_perm_PiE \<pi>)
+        also have "image_mset f \<dots> = Y"
+          using f by (simp add: tuples_def)
+        finally show ?thesis .
+      qed
+      ultimately show "restrict f' (X \<rightarrow>\<^sub>E Roots) \<in> tuples Y"
+        by (auto simp: tuples_def)
+    qed
+    show "(\<lambda>f. restrict (\<lambda>g. f (restrict (\<pi> \<circ> g) X)) (X \<rightarrow>\<^sub>E Roots)) \<in> tuples Y \<rightarrow> tuples Y"
+      by (intro * \<pi>)
+    show "(\<lambda>f. restrict (\<lambda>g. f (restrict (inv_into UNIV \<pi> \<circ> g) X)) (X \<rightarrow>\<^sub>E Roots)) \<in> tuples Y \<rightarrow> tuples Y"
+      by (intro * permutes_inv \<pi>)
+  next
+    have *: "(\<lambda>g\<in>X \<rightarrow>\<^sub>E Roots. (\<lambda>g\<in>X \<rightarrow>\<^sub>E Roots. f (restrict (\<pi> \<circ> g) X))
+                (restrict (inv_into UNIV \<pi> \<circ> g) X)) = f" (is "?lhs = _")
+      if f: "f \<in> tuples Y" and \<pi>: "\<pi> permutes Roots" for f \<pi>
+    proof
+      fix g show "?lhs g = f g"
+      proof (cases "g \<in> X \<rightarrow>\<^sub>E Roots")
+        case True
+        have "restrict (\<pi> \<circ> restrict (inv_into UNIV \<pi> \<circ> g) X) X = g"
+          using True
+          by (intro ext) (auto simp: permutes_inverses[OF \<pi>])
+        thus ?thesis using True
+          by (auto simp: permutes_in_image[OF permutes_inv[OF \<pi>]])
+      qed (use f in \<open>auto simp: tuples_def\<close>)
+    qed
+    show "(\<lambda>g\<in>X \<rightarrow>\<^sub>E Roots. (\<lambda>g\<in>X \<rightarrow>\<^sub>E Roots. f (restrict (\<pi> \<circ> g) X))
+                (restrict (inv_into UNIV \<pi> \<circ> g) X)) = f" if "f \<in> tuples Y" for f
+      using *[OF that \<pi>] .
+    show "(\<lambda>g\<in>X \<rightarrow>\<^sub>E Roots. (\<lambda>g\<in>X \<rightarrow>\<^sub>E Roots. f (restrict (inv_into UNIV \<pi> \<circ> g) X))
+                (restrict (\<pi> \<circ> g) X)) = f" if "f \<in> tuples Y" for f
+      using *[OF that permutes_inv[OF \<pi>]] permutes_inv_inv[OF \<pi>] by simp
+  qed
+
+  text \<open>
+    We show that the coefficients in the expanded new sum are rational -- again using the 
+    fundamental theorem of symmetric polynomials.
+  \<close>
+  define \<beta>' :: "complex multiset \<Rightarrow> complex"
+    where "\<beta>' = (\<lambda>Y. \<Sum>f\<in>tuples Y. \<Prod>g\<in>X \<rightarrow>\<^sub>E Roots. g (f g))"
+
+  have "\<beta>' Y \<in> \<rat>" if Y: "Y \<in> Roots_ms" for Y
+  proof -
+    define Q :: "complex mpoly"
+      where "Q = (\<Sum>f\<in>tuples Y. \<Prod>g\<in>X \<rightarrow>\<^sub>E Roots. Var (unRoot (g (f g))))"
+
+    have "insertion Root Q \<in> \<rat>"
+    proof (rule symmetric_poly_of_roots_in_subring)
+      show "ring_closed (\<rat> :: complex set)"
+        by standard auto
+      then interpret ring_closed "\<rat> :: complex set" .
+      show "\<forall>m. coeff Q m \<in> \<rat>"
+        by (auto simp: Q_def coeff_Var when_def intro!: sum_in_Rats coeff_prod_closed)
+    next
+      show "symmetric_mpoly {..<n} Q"
+        unfolding symmetric_mpoly_def
+      proof safe
+        fix \<pi> assume \<pi>: "\<pi> permutes {..<n}"
+        define \<pi>' where "\<pi>' = convert_perm (inv_into UNIV \<pi>)"
+        have \<pi>': "\<pi>' permutes Roots"
+          unfolding \<pi>'_def by (intro permutes_convert_perm permutes_inv \<pi>)
+        have "mpoly_map_vars \<pi> Q = (\<Sum>f\<in>tuples Y. \<Prod>g\<in>X \<rightarrow>\<^sub>E Roots. Var (\<pi> (unRoot (g (f g)))))"
+          unfolding Q_def by (simp add: permutes_bij[OF \<pi>])
+        also have "\<dots> = (\<Sum>f\<in>tuples Y. \<Prod>g\<in>X \<rightarrow>\<^sub>E Roots. Var (unRoot (g (f (restrict (\<pi>' \<circ> g) X)))))"
+        proof (rule sum.cong, goal_cases)
+          case (2 f)
+          have f: "f \<in> (X \<rightarrow>\<^sub>E Roots) \<rightarrow>\<^sub>E X"
+            using 2 by (auto simp: tuples_def)
+          have "(\<Prod>g\<in>X \<rightarrow>\<^sub>E Roots. Var (\<pi> (unRoot (g (f g))))) =
+                (\<Prod>g\<in>X \<rightarrow>\<^sub>E Roots. Var (\<pi> (unRoot (restrict (\<pi>' \<circ> g) X (f (restrict (\<pi>' \<circ> g) X))))))"
+            using \<pi>' by (intro prod.reindex_bij_betw [symmetric] bij_betw_compose_left_perm_PiE)
+          also have "\<dots> = (\<Prod>g\<in>X \<rightarrow>\<^sub>E Roots. Var (unRoot (g (f (restrict (\<pi>' \<circ> g) X)))))"
+          proof (intro prod.cong refl arg_cong[of _ _ Var])
+            fix g assume g: "g \<in> X \<rightarrow>\<^sub>E Roots"
+            have "restrict (\<pi>' \<circ> g) X \<in> X \<rightarrow>\<^sub>E Roots"
+              using bij_betw_compose_left_perm_PiE[OF \<pi>', of X] g unfolding bij_betw_def by blast
+            hence *: "f (restrict (\<pi>' \<circ> g) X) \<in> X"
+              by (rule PiE_mem[OF f])
+            hence **: "g (f (restrict (\<pi>' \<circ> g) X)) \<in> Roots"
+              by (rule PiE_mem[OF g])
+
+            have "unRoot (restrict (\<pi>' \<circ> g) X (f (restrict (\<pi>' \<circ> g) X))) =
+                   unRoot (Root (inv_into UNIV \<pi> (unRoot (g (f (restrict (\<pi>' \<circ> g) X))))))"
+              using * ** by (subst \<pi>'_def) (auto simp: convert_perm_def)
+            also have "inv_into UNIV \<pi> (unRoot (g (f (restrict (\<pi>' \<circ> g) X)))) \<in> {..<n}"
+              using ** by (subst permutes_in_image[OF permutes_inv[OF \<pi>]]) auto
+            hence "unRoot (Root (inv_into UNIV \<pi> (unRoot (g (f (restrict (\<pi>' \<circ> g) X)))))) =
+                   inv_into UNIV \<pi> (unRoot (g (f (restrict (\<pi>' \<circ> g) X))))"
+              by (intro unRoot_Root) auto
+            also have "\<pi> \<dots> = unRoot (g (f (restrict (\<pi>' \<circ> g) X)))"
+              by (rule permutes_inverses[OF \<pi>])
+            finally show "\<pi> (unRoot (restrict (\<pi>' \<circ> g) X (f (restrict (\<pi>' \<circ> g) X)))) =
+                          unRoot (g (f (restrict (\<pi>' \<circ> g) X)))" .
+          qed
+          finally show ?case .
+        qed simp_all
+        also have "\<dots> = (\<Sum>x\<in>tuples Y. \<Prod>g\<in>X \<rightarrow>\<^sub>E Roots. Var (unRoot (g ((\<lambda>g\<in>X \<rightarrow>\<^sub>E Roots. x (restrict (\<pi>' \<circ> g) X)) g))))"
+          by (intro sum.cong prod.cong refl) auto
+        also have "\<dots> = Q"
+          unfolding Q_def
+          by (rule sum.reindex_bij_betw[OF bij_betw_compose_perm]) (use \<pi>' Y in simp_all)
+        finally show "mpoly_map_vars \<pi> Q = Q" .
+      qed
+    next
+      show "vars Q \<subseteq> {..<n}"
+        unfolding Q_def
+        by (intro order.trans[OF vars_sum] UN_least order.trans[OF vars_prod])
+           (auto simp: vars_Var tuples_def)
+    next
+      define lc where "lc = Polynomial.lead_coeff P"
+      have "lc \<noteq> 0"
+        unfolding lc_def by auto
+      thus "inverse (of_int lc) * (of_int lc :: complex) = 1" and "inverse (of_int lc) \<in> \<rat>"
+        by auto
+      have "rsquarefree (of_int_poly P :: complex poly)"
+        using \<open>squarefree (of_int_poly P :: complex poly)\<close> by (intro squarefree_imp_rsquarefree)
+      hence "of_int_poly P = Polynomial.smult (of_int lc) (\<Prod>x\<in>Roots. [:-x, 1:])"
+        unfolding lc_def of_int_hom.hom_lead_coeff[symmetric] Roots_def
+        by (rule complex_poly_decompose_rsquarefree [symmetric])
+      also have "(\<Prod>x\<in>Roots. [:-x, 1:]) = (\<Prod>i<n. [:-Root i, 1:])"
+        by (rule prod.reindex_bij_betw[OF Root, symmetric])
+      finally show "of_int_poly P = Polynomial.smult (of_int lc) (\<Prod>i<n. [:- Root i, 1:])" .
+    qed auto
+    also have "insertion Root Q = (\<Sum>f\<in>tuples Y. \<Prod>g\<in>X \<rightarrow>\<^sub>E Roots. Root (unRoot (g (f g))))"
+      by (simp add: Q_def insertion_sum insertion_prod)
+    also have "\<dots> = \<beta>' Y"
+      unfolding \<beta>'_def by (intro sum.cong prod.cong refl Root_unRoot) (auto simp: tuples_def)
+    finally show ?thesis .
+  qed
+  hence "\<forall>Y\<in>Roots_ms. \<exists>x. \<beta>' Y = of_rat x"
+    by (auto elim!: Rats_cases)
+  then obtain \<beta>'' :: "complex multiset \<Rightarrow> rat"
+    where \<beta>'': "\<And>Y. Y \<in> Roots_ms \<Longrightarrow> \<beta>' Y = of_rat (\<beta>'' Y)"
+    by metis
+
+  text \<open>
+    We again collect all the terms that happen to have equal exponents and call their
+    coefficients \<open>\<beta>''\<close>:
+  \<close>
+  define \<beta>''' :: "complex \<Rightarrow> rat" where "\<beta>''' = (\<lambda>\<alpha>. \<Sum>Y\<in>Roots_ms. (\<beta>'' Y when \<Sum>\<^sub>#Y = \<alpha>))"
+  have supp_\<beta>''': "{x. \<beta>''' x \<noteq> 0} \<subseteq> sum_mset ` Roots_ms"
+    by (auto simp: \<beta>'''_def when_def elim!: sum.not_neutral_contains_not_neutral split: if_splits)
+
+  text \<open>
+    We again start with the sum that we now to be zero and multiply it with all the sums that can
+    be obtained with different choices for the roots.
+  \<close>
+  have "0 = (\<Sum>x\<in>X. \<beta> x * exp x)"
+    using sum0 ..
+  also have "\<dots> = (\<Sum>x\<in>X. restrict \<beta> X x * exp x)"
+    by (intro sum.cong) auto
+  also have "\<dots> dvd (\<Prod>f \<in> X \<rightarrow>\<^sub>E Roots. \<Sum>x\<in>X. f x * exp x)"
+    by (rule dvd_prodI) (use \<open>\<beta> ` X \<subseteq> Roots\<close> in \<open>auto simp: id_def\<close>)
+  also have "\<dots> = (\<Sum>f\<in>(X \<rightarrow>\<^sub>E Roots) \<rightarrow>\<^sub>E X. \<Prod>g\<in>X \<rightarrow>\<^sub>E Roots. g (f g) * exp (f g))"
+    by (rule prod_sum_PiE) auto
+  also have "\<dots> = (\<Sum>f\<in>(X \<rightarrow>\<^sub>E Roots) \<rightarrow>\<^sub>E X. (\<Prod>g\<in>X \<rightarrow>\<^sub>E Roots. g (f g)) * exp (\<Sum>g\<in>X \<rightarrow>\<^sub>E Roots. f g))"
+    by (simp add: prod.distrib exp_sum)
+  also have "\<dots> = (\<Sum>(Y,f)\<in>Sigma Roots_ms tuples.
+                    (\<Prod>g\<in>X \<rightarrow>\<^sub>E Roots. g (f g)) * exp (\<Sum>g\<in>X \<rightarrow>\<^sub>E Roots. f g))"
+    by (intro sum.reindex_bij_witness[of _ snd "\<lambda>f. (image_mset f (mset_set (X \<rightarrow>\<^sub>E Roots)), f)"])
+       (auto simp: Roots_ms_def tuples_def)
+  also have "\<dots> = (\<Sum>(Y,f)\<in>Sigma Roots_ms tuples. (\<Prod>g\<in>X \<rightarrow>\<^sub>E Roots. g (f g)) * exp (\<Sum>\<^sub>#Y))"
+    by (intro sum.cong) (auto simp: tuples_def sum_unfold_sum_mset)
+  also have "\<dots> = (\<Sum>Y\<in>Roots_ms. \<beta>' Y * exp (\<Sum>\<^sub>#Y))"
+    unfolding \<beta>'_def sum_distrib_right by (rule sum.Sigma [symmetric]) auto
+  also have "\<dots> = (\<Sum>Y\<in>Roots_ms. of_rat (\<beta>'' Y) * exp (\<Sum>\<^sub>#Y))"
+    by (intro sum.cong) (auto simp: \<beta>'')
+  also have "\<dots> = (\<Sum>Y\<in>Roots_ms. Sum_any (\<lambda>\<alpha>. of_rat (\<beta>'' Y when \<Sum>\<^sub># Y = \<alpha>) * exp \<alpha>))"
+  proof (rule sum.cong, goal_cases)
+    case (2 Y)
+    have "Sum_any (\<lambda>\<alpha>. of_rat (\<beta>'' Y when \<Sum>\<^sub># Y = \<alpha>) * exp \<alpha>) =
+          (\<Sum>\<alpha>\<in>{\<Sum>\<^sub># Y}. of_rat (\<beta>'' Y when \<Sum>\<^sub># Y = \<alpha>) * exp \<alpha>)"
+      by (intro Sum_any.expand_superset) auto
+    thus ?case by simp
+  qed auto
+  also have "\<dots> = Sum_any (\<lambda>\<alpha>. of_rat (\<beta>''' \<alpha>) * exp \<alpha>)"
+    unfolding \<beta>'''_def of_rat_sum sum_distrib_right by (subst Sum_any_sum_swap) auto
+  also have "\<dots> = (\<Sum>\<alpha> | \<beta>''' \<alpha> \<noteq> 0. of_rat (\<beta>''' \<alpha>) * exp \<alpha>)"
+    by (intro Sum_any.expand_superset finite_subset[OF supp_\<beta>''']) auto
+  finally have "(\<Sum>\<alpha> | \<beta>''' \<alpha> \<noteq> 0. of_rat (\<beta>''' \<alpha>) * exp \<alpha>) = 0"
+    by auto
+
+  text \<open>
+    We are now in the situation of our previous version of the theorem and can apply it to find
+    that all the coefficients are zero.
+  \<close>
+  have "{\<alpha>. \<beta>''' \<alpha> \<noteq> 0} = {}"
+  proof (rule Hermite_Lindemann_aux3)
+    show "finite {\<alpha>. \<beta>''' \<alpha> \<noteq> 0}"
+      by (rule finite_subset[OF supp_\<beta>''']) auto
+  next
+    show "(\<Sum>\<alpha> | \<beta>''' \<alpha> \<noteq> 0. of_rat (\<beta>''' \<alpha>) * exp \<alpha>) = 0"
+    by fact
+  next
+    fix \<alpha> assume \<alpha>: "\<alpha> \<in> {\<alpha>. \<beta>''' \<alpha> \<noteq> 0}"
+    then obtain Y where Y: "Y \<in> Roots_ms" "\<alpha> = sum_mset Y"
+      using supp_\<beta>''' by auto
+    thus "algebraic \<alpha>" using alg1
+      by (auto simp: Roots_ms_def)
+  qed auto
+
+  text \<open>
+    However, similarly to before, we can show that the coefficient corresponding to the
+    term with the lexicographically greatest exponent (which is obtained by picking the
+    term with the lexicographically greatest term in each of the factors of our big product)
+    is non-zero.
+  \<close>
+  moreover have "\<exists>\<alpha>. \<beta>''' \<alpha> \<noteq> 0"
+  proof -
+    define \<alpha>_max where "\<alpha>_max = complex_lex.Max X"
+    have [simp]: "\<alpha>_max \<in> X"
+      unfolding \<alpha>_max_def using \<open>X \<noteq> {}\<close> by (intro complex_lex.Max_in) auto
+    define Y_max :: "complex multiset" where "Y_max = replicate_mset (n ^ m) \<alpha>_max"
+    define f_max where "f_max = restrict (\<lambda>_. \<alpha>_max) (X \<rightarrow>\<^sub>E Roots)"
+    have [simp]: "Y_max \<in> Roots_ms"
+      by (auto simp: Y_max_def Roots_ms_def)
+    have "tuples Y_max = {f_max}"
+    proof safe
+      have "image_mset (\<lambda>_\<in>X \<rightarrow>\<^sub>E Roots. \<alpha>_max) (mset_set (X \<rightarrow>\<^sub>E Roots)) =
+            image_mset (\<lambda>_. \<alpha>_max) (mset_set (X \<rightarrow>\<^sub>E Roots))"
+        by (intro image_mset_cong) auto
+      thus "f_max \<in> tuples Y_max"
+        by (auto simp: f_max_def tuples_def Y_max_def image_mset_const_eq)
+    next
+      fix f assume "f \<in> tuples Y_max"
+      hence f: "f \<in> (X \<rightarrow>\<^sub>E Roots) \<rightarrow>\<^sub>E X" "image_mset f (mset_set (X \<rightarrow>\<^sub>E Roots)) = Y_max"
+        by (auto simp: tuples_def)
+      hence "\<forall>g \<in># mset_set (X \<rightarrow>\<^sub>E Roots). f g = \<alpha>_max"
+        by (intro image_mset_eq_replicate_msetD[where n = "n ^ m"]) (auto simp: Y_max_def)
+      thus "f = f_max"
+        using f by (auto simp: Y_max_def fun_eq_iff f_max_def)
+    qed
+
+    have "\<beta>''' (of_nat (n ^ m) * \<alpha>_max) = (\<Sum>Y\<in>Roots_ms. \<beta>'' Y when \<Sum>\<^sub># Y = of_nat (n ^ m) * \<alpha>_max)"
+      unfolding \<beta>'''_def Roots_ms_def ..
+    also have "\<Sum>\<^sub># Y \<noteq> of_nat n ^ m * \<alpha>_max" if "Y \<in> Roots_ms" "Y \<noteq> Y_max" for Y
+    proof -
+      have "\<not>set_mset Y \<subseteq> {\<alpha>_max}"
+        using set_mset_subset_singletonD[of Y "\<alpha>_max"] that
+        by (auto simp: Roots_ms_def Y_max_def split: if_splits)
+      then obtain y where y: "y \<in># Y" "y \<noteq> \<alpha>_max"
+        by auto
+      have "y \<in> X" "set_mset (Y - {#y#}) \<subseteq> X"
+        using y that by (auto simp: Roots_ms_def dest: in_diffD)
+      hence "y \<le>\<^sub>\<complex> \<alpha>_max"
+        using y unfolding \<alpha>_max_def by (intro complex_lex.Max_ge) auto
+      with y have "y <\<^sub>\<complex> \<alpha>_max"
+        by auto
+      have *: "Y = {#y#} + (Y - {#y#})"
+        using y by simp
+      have "sum_mset Y = y + sum_mset (Y - {#y#})"
+        by (subst *) auto
+      also have "\<dots> <\<^sub>\<complex> \<alpha>_max + sum_mset (Y - {#y#})"
+        by (intro complex_lex.add_strict_right_mono) fact
+      also have "\<dots> \<le>\<^sub>\<complex> \<alpha>_max + sum_mset (replicate_mset (n ^ m - 1) \<alpha>_max)"
+        unfolding \<alpha>_max_def using that y \<open>set_mset (Y - {#y#}) \<subseteq> X\<close>
+        by (intro complex_lex.add_left_mono sum_mset_mono_complex_lex
+                  rel_mset_replicate_mset_right complex_lex.Max_ge)
+           (auto simp: Roots_ms_def size_Diff_singleton)
+      also have "\<dots> = of_nat (Suc (n ^ m - 1)) * \<alpha>_max"
+        by (simp add: algebra_simps)
+      also have "Suc (n ^ m - 1) = n ^ m"
+        using \<open>n > 0\<close> by simp
+      finally show ?thesis by simp
+    qed
+    hence "(\<Sum>Y\<in>Roots_ms. \<beta>'' Y when \<Sum>\<^sub># Y = of_nat (n ^ m) * \<alpha>_max) = (\<Sum>Y\<in>{Y_max}. \<beta>'' Y when \<Sum>\<^sub># Y = of_nat (n ^ m) * \<alpha>_max)"
+      by (intro sum.mono_neutral_right ballI) auto
+    also have "\<dots> = \<beta>'' Y_max"
+      by (auto simp: when_def Y_max_def)
+    also have "of_rat \<dots> = \<beta>' Y_max"
+      using \<beta>''[of Y_max] by auto
+    also have "\<dots> = (\<Prod>g\<in>X \<rightarrow>\<^sub>E Roots. g (f_max g))"
+      by (auto simp: \<beta>'_def \<open>tuples Y_max = {f_max}\<close>)
+    also have "\<dots> = (\<Prod>g\<in>X \<rightarrow>\<^sub>E Roots. g \<alpha>_max)"
+      by (intro prod.cong) (auto simp: f_max_def)
+    also have "\<dots> \<noteq> 0"
+      using \<open>0 \<notin> Roots\<close> \<open>\<alpha>_max \<in> X\<close> by (intro prod_nonzeroI) (metis PiE_mem)
+    finally show ?thesis by blast
+  qed
+
+  ultimately show False by blast
+qed
+
+
+subsection \<open>The final theorem\<close>
+
+text \<open>
+  We now additionally allow some of the $\beta_i$ to be zero:
+\<close>
+lemma Hermite_Lindemann':
+  fixes \<beta> :: "complex \<Rightarrow> complex"
+  assumes "finite X"
+  assumes "\<And>x. x \<in> X \<Longrightarrow> algebraic x"
+  assumes "\<And>x. x \<in> X \<Longrightarrow> algebraic (\<beta> x)"
+  assumes "(\<Sum>x\<in>X. \<beta> x * exp x) = 0"
+  shows   "\<forall>x\<in>X. \<beta> x = 0"
+proof -
+  have "{x\<in>X. \<beta> x \<noteq> 0} = {}"
+  proof (rule Hermite_Lindemann_aux4)
+    have "(\<Sum>x | x \<in> X \<and> \<beta> x \<noteq> 0. \<beta> x * exp x) = (\<Sum>x\<in>X. \<beta> x * exp x)"
+      by (intro sum.mono_neutral_left assms(1)) auto
+    also have "\<dots> = 0"
+      by fact
+    finally show "(\<Sum>x | x \<in> X \<and> \<beta> x \<noteq> 0. \<beta> x * exp x) = 0" .
+  qed (use assms in auto)
+  thus ?thesis by blast
+qed
+
+text \<open>
+  Lastly, we switch to indexed summation in order to obtain a version of the theorem that
+  is somewhat nicer to use:
+\<close>
+theorem Hermite_Lindemann:
+  fixes \<alpha> \<beta> :: "'a \<Rightarrow> complex"
+  assumes "finite I"
+  assumes "\<And>x. x \<in> I \<Longrightarrow> algebraic (\<alpha> x)"
+  assumes "\<And>x. x \<in> I \<Longrightarrow> algebraic (\<beta> x)"
+  assumes "inj_on \<alpha> I"
+  assumes "(\<Sum>x\<in>I. \<beta> x * exp (\<alpha> x)) = 0"
+  shows   "\<forall>x\<in>I. \<beta> x = 0"
+proof -
+  define f where "f = inv_into I \<alpha>"
+  have [simp]: "f (\<alpha> x) = x" if "x \<in> I" for x
+    using that by (auto simp: f_def inv_into_f_f[OF assms(4)])
+  have "\<forall>x\<in>\<alpha>`I. (\<beta> \<circ> f) x = 0"
+  proof (rule Hermite_Lindemann')
+    have "0 = (\<Sum>x\<in>I. \<beta> x * exp (\<alpha> x))"
+      using assms(5) ..
+    also have "\<dots> = (\<Sum>x\<in>I. (\<beta> \<circ> f) (\<alpha> x) * exp (\<alpha> x))"
+      by (intro sum.cong) auto
+    also have "\<dots> = (\<Sum>x\<in>\<alpha>`I. (\<beta> \<circ> f) x * exp x)"
+      using assms(4) by (subst sum.reindex) auto
+    finally show "(\<Sum>x\<in>\<alpha> ` I. (\<beta> \<circ> f) x * exp x) = 0" ..
+  qed (use assms in auto)
+  thus ?thesis by auto
+qed
+
+text \<open>
+  The following version using lists instead of sequences is even more convenient to use
+  in practice:
+\<close>
+corollary Hermite_Lindemann_list:
+  fixes xs :: "(complex \<times> complex) list"
+  assumes alg:      "\<forall>(x,y)\<in>set xs. algebraic x \<and> algebraic y"
+  assumes distinct: "distinct (map snd xs)"
+  assumes sum0:     "(\<Sum>(c,\<alpha>)\<leftarrow>xs. c * exp \<alpha>) = 0"
+  shows   "\<forall>c\<in>(fst ` set xs). c = 0"
+proof -
+  define n where "n = length xs"
+  have *: "\<forall>i\<in>{..<n}. fst (xs ! i) = 0"
+  proof (rule Hermite_Lindemann)
+    from distinct have "inj_on (\<lambda>i. map snd xs ! i) {..<n}"
+      by (intro inj_on_nth) (auto simp: n_def)
+    also have "?this \<longleftrightarrow> inj_on (\<lambda>i. snd (xs ! i)) {..<n}"
+      by (intro inj_on_cong) (auto simp: n_def)
+    finally show "inj_on (\<lambda>i. snd (xs ! i)) {..<n}" .
+  next
+    have "0 = (\<Sum>(c,\<alpha>)\<leftarrow>xs. c * exp \<alpha>)"
+      using sum0 ..
+    also have "\<dots> = (\<Sum>i<n. fst (xs ! i) * exp (snd (xs ! i)))"
+      unfolding sum_list_sum_nth
+      by (intro sum.cong) (auto simp: n_def case_prod_unfold)
+    finally show "\<dots> = 0" ..
+  next
+    fix i assume i: "i \<in> {..<n}"
+    hence "(fst (xs ! i), snd (xs ! i)) \<in> set xs"
+      by (auto simp: n_def)
+    with alg show "algebraic (fst (xs ! i))" "algebraic (snd (xs ! i))"
+      by blast+
+  qed auto
+
+  show ?thesis
+  proof (intro ballI, elim imageE)
+    fix c x assume cx: "c = fst x" "x \<in> set xs"
+    then obtain i where "i \<in> {..<n}" "x = xs ! i"
+      by (auto simp: set_conv_nth n_def)
+    with * cx show "c = 0" by blast
+  qed
+qed
+
+
+subsection \<open>The traditional formulation of the theorem\<close>
+
+text \<open>
+  What we proved above was actually Baker's reformulation of the theorem. Thus, we now also derive
+  the original one, which uses linear independence and algebraic independence.
+
+  It states that if $\alpha_1, \ldots, \alpha_n$ are algebraic numbers that are linearly
+  independent over \<open>\<int>\<close>, then $e^{\alpha_1}, \ldots, e^{\alpha_n}$ are algebraically independent
+  over \<open>\<rat>\<close>.
+\<close>
+
+text \<open>
+  Linear independence over the integers is just independence of a set of complex numbers when
+  viewing the complex numbers as a \<open>\<int>\<close>-module.
+\<close>
+definition linearly_independent_over_int :: "'a :: field_char_0 set \<Rightarrow> bool" where
+  "linearly_independent_over_int = module.independent (\<lambda>r x. of_int r * x)"
+
+text \<open>
+  Algebraic independence over the rationals means that the given set \<open>X\<close> of numbers fulfils
+  no non-trivial polynomial equation with rational coefficients, i.e. there is no non-zero
+  multivariate polynomial with rational coefficients that, when inserting the numbers from \<open>X\<close>,
+  becomes zero.
+
+  Note that we could easily replace `rational coefficients' with `algebraic coefficients' here
+  and the proof would still go through without any modifications.
+\<close>
+definition algebraically_independent_over_rat :: "nat \<Rightarrow> (nat \<Rightarrow> 'a :: field_char_0) \<Rightarrow> bool" where
+  "algebraically_independent_over_rat n a \<longleftrightarrow>
+     (\<forall>p. vars p \<subseteq> {..<n} \<and> (\<forall>m. coeff p m \<in> \<rat>) \<and> insertion a p = 0 \<longrightarrow> p = 0)"
+
+corollary Hermite_Lindemann_original:
+  fixes n :: nat and \<alpha> :: "nat \<Rightarrow> complex"
+  assumes "inj_on \<alpha> {..<n}"
+  assumes "\<And>i. i < n \<Longrightarrow> algebraic (\<alpha> i)"
+  assumes "linearly_independent_over_int (\<alpha> ` {..<n})"
+  shows   "algebraically_independent_over_rat n (\<lambda>i. exp (\<alpha> i))"
+  unfolding algebraically_independent_over_rat_def
+proof safe
+  fix p assume p: "vars p \<subseteq> {..<n}" "\<forall>m. coeff p m \<in> \<rat>" "insertion (\<lambda>i. exp (\<alpha> i)) p = 0"
+  define \<alpha>' where "\<alpha>' = (\<lambda>m. \<Sum>i<n. of_nat (lookup m i) * \<alpha> i)"
+  define I where "I = {m. coeff p m \<noteq> 0}"
+
+  have lookup_eq_0: "lookup m i = 0" if "m \<in> I" "i \<notin> {..<n}" for i m
+  proof -
+    have "keys m \<subseteq> vars p"
+      using that coeff_notin_vars[of m p] by (auto simp: I_def)
+    thus "lookup m i = 0"
+      using in_keys_iff[of i m] that p(1) by blast
+  qed
+
+  have "\<forall>x\<in>I. coeff p x = 0"
+  proof (rule Hermite_Lindemann)
+    show "finite I"
+      by (auto simp: I_def)
+  next
+    show "algebraic (\<alpha>' m)" if "m \<in> I" for m
+      unfolding \<alpha>'_def using assms(2) by fastforce
+  next
+    show "algebraic (coeff p m)" if "m \<in> I" for m
+      unfolding \<alpha>'_def using p(2) by blast
+  next
+    show "inj_on \<alpha>' I"
+    proof
+      fix m1 m2 assume m12: "m1 \<in> I" "m2 \<in> I" "\<alpha>' m1 = \<alpha>' m2"
+      define lu :: "(nat \<Rightarrow>\<^sub>0 nat) \<Rightarrow> nat \<Rightarrow> int" where "lu = (\<lambda>m i. int (lookup m i))"
+      interpret int: Modules.module "\<lambda>r x. of_int r * (x :: complex)"
+        by standard (auto simp: algebra_simps of_rat_mult of_rat_add)
+      define idx where "idx = inv_into {..<n} \<alpha>"
+
+      have "lu m1 i = lu m2 i" if "i < n" for i
+      proof -
+        have "lu m1 (idx (\<alpha> i)) - lu m2 (idx (\<alpha> i)) = 0"
+        proof (rule int.independentD)
+          show "int.independent (\<alpha> ` {..<n})"
+            using assms(3) by (simp add: linearly_independent_over_int_def)
+        next
+          have "(\<Sum>x\<in>\<alpha>`{..<n}. of_int (lu m1 (idx x) - lu m2 (idx x)) * x) =
+                (\<Sum>i<n. of_int (lu m1 (idx (\<alpha> i)) - lu m2 (idx (\<alpha> i))) * \<alpha> i)"
+            using assms(1) by (subst sum.reindex) auto
+          also have "\<dots> = (\<Sum>i<n. of_int (lu m1 i - lu m2 i) * \<alpha> i)"
+            by (intro sum.cong) (auto simp: idx_def inv_into_f_f[OF assms(1)])
+          also have "\<dots> = 0"
+            using m12 by (simp add: \<alpha>'_def ring_distribs of_rat_diff sum_subtractf lu_def)
+          finally show "(\<Sum>x\<in>\<alpha>`{..<n}. of_int (lu m1 (idx x) - lu m2 (idx x)) * x) = 0"
+            by (simp add: \<alpha>'_def ring_distribs of_rat_diff sum_subtractf lu_def)
+        qed (use that in auto)
+        thus ?thesis
+          using that by (auto simp: idx_def inv_into_f_f[OF assms(1)])
+      qed
+      hence "lookup m1 i = lookup m2 i" for i
+        using m12 by (cases "i < n") (auto simp: lu_def lookup_eq_0)
+      thus "m1 = m2"
+        by (rule poly_mapping_eqI)
+    qed
+  next
+    have "0 = insertion (\<lambda>i. exp (\<alpha> i)) p"
+      using p(3) ..
+    also have "\<dots> = (\<Sum>m\<in>I. coeff p m * Prod_any (\<lambda>i. exp (\<alpha> i) ^ lookup m i))"
+      unfolding insertion_altdef by (rule Sum_any.expand_superset) (auto simp: I_def)
+    also have "\<dots> = (\<Sum>m\<in>I. coeff p m * exp (\<alpha>' m))"
+    proof (intro sum.cong, goal_cases)
+      case (2 m)
+      have "Prod_any (\<lambda>i. exp (\<alpha> i) ^ lookup m i) = (\<Prod>i<n. exp (\<alpha> i) ^ lookup m i)"
+        using 2 lookup_eq_0[of m] by (intro Prod_any.expand_superset; force)
+      also have "\<dots> = exp (\<alpha>' m)"
+        by (simp add: exp_sum exp_of_nat_mult \<alpha>'_def)
+      finally show ?case by simp
+    qed simp_all
+    finally show "(\<Sum>m\<in>I. coeff p m * exp (\<alpha>' m)) = 0" ..
+  qed
+  thus "p = 0"
+    by (intro mpoly_eqI) (auto simp: I_def)
+qed
+
+
+subsection \<open>Simple corollaries\<close>
+
+text \<open>
+  Now, we derive all the usual obvious corollaries of the theorem in the obvious way.
+
+  First, the exponential of a non-zero algebraic number is transcendental.
+\<close>
+corollary algebraic_exp_complex_iff:
+  assumes "algebraic x"
+  shows   "algebraic (exp x :: complex) \<longleftrightarrow> x = 0"
+  using Hermite_Lindemann_list[of "[(1, x), (-exp x, 0)]"] assms by auto
+
+text \<open>
+  More generally, any sum of exponentials with algebraic coefficients and exponents is
+  transcendental if the exponents are all distinct and non-zero and at least one coefficient
+  is non-zero.
+\<close>
+corollary sum_of_exp_transcendentalI:
+  fixes xs :: "(complex \<times> complex) list"
+  assumes "\<forall>(x,y)\<in>set xs. algebraic x \<and> algebraic y \<and> y \<noteq> 0"
+  assumes "\<exists>x\<in>fst`set xs. x \<noteq> 0"
+  assumes distinct: "distinct (map snd xs)"
+  shows   "\<not>algebraic (\<Sum>(c,\<alpha>)\<leftarrow>xs. c * exp \<alpha>)"
+proof
+  define S where "S = (\<Sum>(c,\<alpha>)\<leftarrow>xs. c * exp \<alpha>)"
+  assume S: "algebraic S"
+  have "\<forall>c\<in>fst`set ((-S,0) # xs). c = 0"
+  proof (rule Hermite_Lindemann_list)
+    show "(\<Sum>(c, \<alpha>)\<leftarrow>(- S, 0) # xs. c * exp \<alpha>) = 0"
+      by (auto simp: S_def)
+  qed (use S assms in auto)
+  with assms(2) show False
+    by auto
+qed
+
+text \<open>
+  Any complex logarithm of an algebraic number other than 1 is transcendental
+  (no matter which branch cut).
+\<close>
+corollary transcendental_complex_logarithm:
+  assumes "algebraic x" "exp y = (x :: complex)" "x \<noteq> 1"
+  shows   "\<not>algebraic y"
+  using algebraic_exp_complex_iff[of y] assms by auto
+
+text \<open>
+  In particular, this holds for the standard branch of the logarithm.
+\<close>
+corollary transcendental_Ln:
+  assumes "algebraic x" "x \<noteq> 0" "x \<noteq> 1"
+  shows   "\<not>algebraic (Ln x)"
+  by (rule transcendental_complex_logarithm) (use assms in auto)
+
+text \<open>
+  The transcendence of \<open>e\<close> and \<open>\<pi>\<close>, which I have already formalised directly in other AFP
+  entries, now follows as a simple corollary.
+\<close>
+corollary exp_1_complex_transcendental: "\<not>algebraic (exp 1 :: complex)"
+  by (subst algebraic_exp_complex_iff) auto
+
+corollary pi_transcendental: "\<not>algebraic pi"
+proof -
+  have "\<not>algebraic (\<i> * pi)"
+    by (rule transcendental_complex_logarithm[of "-1"]) auto
+  thus ?thesis by simp
+qed
+
+
+subsection \<open>Transcendence of the trigonometric and hyperbolic functions\<close>
+
+text \<open>
+  In a similar fashion, we can also prove the transcendence of all the trigonometric and
+  hyperbolic functions such as $\sin$, $\tan$, $\sinh$, $\arcsin$, etc.
+\<close>
+
+lemma transcendental_sinh:
+  assumes "algebraic z" "z \<noteq> 0"
+  shows   "\<not>algebraic (sinh z :: complex)"
+proof -
+  have "\<not>algebraic (\<Sum>(a,b)\<leftarrow>[(1/2, z), (-1/2, -z)]. a * exp b)"
+    using assms by (intro sum_of_exp_transcendentalI) auto
+  also have "(\<Sum>(a,b)\<leftarrow>[(1/2, z), (-1/2, -z)]. a * exp b) = sinh z"
+    by (simp add: sinh_def field_simps scaleR_conv_of_real)
+  finally show ?thesis .
+qed
+
+lemma transcendental_cosh:
+  assumes "algebraic z" "z \<noteq> 0"
+  shows   "\<not>algebraic (cosh z :: complex)"
+proof -
+  have "\<not>algebraic (\<Sum>(a,b)\<leftarrow>[(1/2, z), (1/2, -z)]. a * exp b)"
+    using assms by (intro sum_of_exp_transcendentalI) auto
+  also have "(\<Sum>(a,b)\<leftarrow>[(1/2, z), (1/2, -z)]. a * exp b) = cosh z"
+    by (simp add: cosh_def field_simps scaleR_conv_of_real)
+  finally show ?thesis .
+qed
+
+lemma transcendental_sin:
+  assumes "algebraic z" "z \<noteq> 0"
+  shows   "\<not>algebraic (sin z :: complex)"
+  unfolding sin_conv_sinh using transcendental_sinh[of "\<i> * z"] assms by simp
+
+lemma transcendental_cos:
+  assumes "algebraic z" "z \<noteq> 0"
+  shows   "\<not>algebraic (cos z :: complex)"
+  unfolding cos_conv_cosh using transcendental_cosh[of "\<i> * z"] assms by simp
+
+(* TODO: Move? *)
+lemma tan_square_neq_neg1: "tan (z :: complex) ^ 2 \<noteq> -1"
+proof
+  assume "tan z ^ 2 = -1"
+  hence "sin z ^ 2 = -(cos z ^ 2)"
+    by (auto simp: tan_def divide_simps split: if_splits)
+  also have "cos z ^ 2 = 1 - sin z ^ 2"
+    by (simp add: cos_squared_eq)
+  finally show False
+    by simp
+qed
+
+lemma transcendental_tan:
+  assumes "algebraic z" "z \<noteq> 0"
+  shows   "\<not>algebraic (tan z :: complex)"
+proof
+  assume "algebraic (tan z)"
+
+  have nz1: "real_of_int n + 1 / 2 \<noteq> 0" for n
+  proof -
+    have "real_of_int (2 * n + 1) / real_of_int 2 \<notin> \<int>"
+      by (intro fraction_not_in_ints) auto
+    also have "real_of_int (2 * n + 1) / real_of_int 2 = real_of_int n + 1 / 2"
+      by simp
+    finally show "\<dots> \<noteq> 0"
+      by auto
+  qed
+
+  have nz2: "1 + tan z ^ 2 \<noteq> 0"
+    using tan_square_neq_neg1[of z] by (subst add_eq_0_iff) 
+
+  have nz3: "cos z \<noteq> 0"
+  proof
+    assume "cos z = 0"
+    then obtain n where "z = complex_of_real (real_of_int n * pi) + complex_of_real pi / 2"
+      by (subst (asm) cos_eq_0) blast
+    also have "\<dots> = complex_of_real ((real_of_int n + 1 / 2) * pi)"
+      by (simp add: ring_distribs)
+    also have "algebraic \<dots> \<longleftrightarrow> algebraic ((real_of_int n + 1 / 2) * pi)"
+      by (rule algebraic_of_real_iff)
+    also have "\<not>algebraic ((real_of_int n + 1 / 2) * pi)"
+      using nz1[of n] transcendental_pi by simp
+    finally show False using assms(1) by contradiction
+  qed
+
+  from nz3 have *: "sin z ^ 2 = tan z ^ 2 * cos z ^ 2"
+    by (simp add: tan_def field_simps)
+  also have "cos z ^ 2 = 1 - sin z ^ 2"
+    by (simp add: cos_squared_eq)
+  finally have "sin z ^ 2 * (1 + tan z ^ 2) = tan z ^ 2"
+    by (simp add: algebra_simps)
+  hence "sin z ^ 2 = tan z ^ 2 / (1 + tan z ^ 2)"
+    using nz2 by (simp add: field_simps)
+  also have "algebraic (tan z ^ 2 / (1 + tan z ^ 2))"
+    using \<open>algebraic (tan z)\<close> by auto
+  finally have "algebraic (sin z ^ 2)" .
+  hence "algebraic (sin z)"
+    by simp
+  thus False
+    using transcendental_sin[OF \<open>algebraic z\<close> \<open>z \<noteq> 0\<close>] by contradiction
+qed
+
+lemma transcendental_cot:
+  assumes "algebraic z" "z \<noteq> 0"
+  shows   "\<not>algebraic (cot z :: complex)"
+proof -
+  have "\<not>algebraic (tan z)"
+    by (rule transcendental_tan) fact+
+  also have "algebraic (tan z) \<longleftrightarrow> algebraic (inverse (tan z))"
+    by simp
+  also have "inverse (tan z) = cot z"
+    by (simp add: cot_def tan_def)
+  finally show ?thesis .
+qed
+
+lemma transcendental_tanh:
+  assumes "algebraic z" "z \<noteq> 0" "cosh z \<noteq> 0"
+  shows   "\<not>algebraic (tanh z :: complex)"
+  using transcendental_tan[of "\<i> * z"] assms unfolding tanh_conv_tan by simp
+
+lemma transcendental_Arcsin:
+  assumes "algebraic z" "z \<noteq> 0"
+  shows   "\<not>algebraic (Arcsin z)"
+proof -
+  have "\<i> * z + csqrt (1 - z\<^sup>2) \<noteq> 0"
+    using Arcsin_body_lemma by blast
+  moreover have "\<i> * z + csqrt (1 - z\<^sup>2) \<noteq> 1"
+  proof
+    assume "\<i> * z + csqrt (1 - z\<^sup>2) = 1"
+    hence "Arcsin z = 0"
+      by (simp add: Arcsin_def)
+    hence "sin (Arcsin z) = 0"
+      by (simp only: sin_zero)
+    also have "sin (Arcsin z) = z"
+      by simp
+    finally show False using \<open>z \<noteq> 0\<close> by simp
+  qed
+  ultimately have "\<not> algebraic (Ln (\<i> * z + csqrt (1 - z\<^sup>2)))"
+    using assms by (intro transcendental_Ln) auto
+  thus ?thesis
+    by (simp add: Arcsin_def)
+qed
+
+lemma transcendental_Arccos:
+  assumes "algebraic z" "z \<noteq> 1"
+  shows   "\<not>algebraic (Arccos z)"
+proof -
+  have "z + \<i> * csqrt (1 - z\<^sup>2) \<noteq> 0"
+    using Arccos_body_lemma by blast
+  moreover have "z + \<i> * csqrt (1 - z\<^sup>2) \<noteq> 1"
+  proof
+    assume "z + \<i> * csqrt (1 - z\<^sup>2) = 1"
+    hence "Arccos z = 0"
+      by (simp add: Arccos_def)
+    hence "cos (Arccos z) = 1"
+      by (simp only: cos_zero)
+    also have "cos (Arccos z) = z"
+      by simp
+    finally show False using \<open>z \<noteq> 1\<close> by simp
+  qed
+  ultimately have "\<not> algebraic (Ln (z + \<i> * csqrt (1 - z\<^sup>2)))"
+    using assms by (intro transcendental_Ln) auto
+  thus ?thesis
+    by (simp add: Arccos_def)
+qed
+
+lemma transcendental_Arctan:
+  assumes "algebraic z" "z \<notin> {0, \<i>, -\<i>}"
+  shows   "\<not>algebraic (Arctan z)"
+proof -
+  have "\<i> * z \<noteq> 1" "1 + \<i> * z \<noteq> 0"
+    using assms(2) by (auto simp: complex_eq_iff)
+  hence "\<not> algebraic (Ln ((1 - \<i> * z) / (1 + \<i> * z)))"
+    using assms by (intro transcendental_Ln) auto
+  thus ?thesis
+    by (simp add: Arctan_def)
+qed
+
+end
\ No newline at end of file
diff --git a/thys/Hermite_Lindemann/Min_Int_Poly.thy b/thys/Hermite_Lindemann/Min_Int_Poly.thy
new file mode 100644
--- /dev/null
+++ b/thys/Hermite_Lindemann/Min_Int_Poly.thy
@@ -0,0 +1,190 @@
+(*
+  File:     Min_Int_Poly.thy
+  Author:   Manuel Eberl, TU München
+*)
+section \<open>The minimal polynomial of an algebraic number\<close>
+theory Min_Int_Poly
+imports
+  "Algebraic_Numbers.Algebraic_Numbers"
+  "HOL-Computational_Algebra.Computational_Algebra"
+  More_Polynomial_HLW
+begin
+
+text \<open>
+  Given an algebraic number \<open>x\<close> in a field, the minimal polynomial is the unique irreducible
+  integer polynomial with positive leading coefficient that has \<open>x\<close> as a root.
+
+  Note that we assume characteristic 0 since the material upon which all of this builds also
+  assumes it.
+\<close>
+
+(* TODO Move *)
+
+definition min_int_poly :: "'a :: field_char_0 \<Rightarrow> int poly" where
+  "min_int_poly x =
+     (if algebraic x then THE p. p represents x \<and> irreducible p \<and> Polynomial.lead_coeff p > 0
+      else [:0, 1:])"
+
+lemma
+  fixes x :: "'a :: {field_char_0, field_gcd}"
+  shows min_int_poly_represents [intro]: "algebraic x \<Longrightarrow> min_int_poly x represents x"
+  and   min_int_poly_irreducible [intro]: "irreducible (min_int_poly x)"
+  and   lead_coeff_min_int_poly_pos: "Polynomial.lead_coeff (min_int_poly x) > 0"
+proof -
+  note * = theI'[OF algebraic_imp_represents_unique, of x]
+  show "min_int_poly x represents x" if "algebraic x"
+    using *[OF that] by (simp add: that min_int_poly_def)
+  have "irreducible [:0, 1::int:]"
+    by (rule irreducible_linear_poly) auto
+  thus "irreducible (min_int_poly x)"
+    using * by (auto simp: min_int_poly_def)
+  show "Polynomial.lead_coeff (min_int_poly x) > 0"
+    using * by (auto simp: min_int_poly_def)
+qed
+
+lemma 
+  fixes x :: "'a :: {field_char_0, field_gcd}"
+  shows degree_min_int_poly_pos [intro]: "Polynomial.degree (min_int_poly x) > 0"
+    and degree_min_int_poly_nonzero [simp]: "Polynomial.degree (min_int_poly x) \<noteq> 0"
+proof -
+  show "Polynomial.degree (min_int_poly x) > 0"
+  proof (cases "algebraic x")
+    case True
+    hence "min_int_poly x represents x"
+      by auto
+    thus ?thesis by blast
+  qed (auto simp: min_int_poly_def)
+  thus "Polynomial.degree (min_int_poly x) \<noteq> 0"
+    by blast
+qed
+
+lemma min_int_poly_squarefree [intro]:
+  fixes x :: "'a :: {field_char_0, field_gcd}"
+  shows "squarefree (min_int_poly x)"
+  by (rule irreducible_imp_squarefree) auto
+
+lemma min_int_poly_primitive [intro]:
+  fixes x :: "'a :: {field_char_0, field_gcd}"
+  shows "primitive (min_int_poly x)"
+  by (rule irreducible_imp_primitive) auto
+
+lemma min_int_poly_content [simp]:
+  fixes x :: "'a :: {field_char_0, field_gcd}"
+  shows "content (min_int_poly x) = 1"
+  using min_int_poly_primitive[of x] by (simp add: primitive_def)
+
+lemma ipoly_min_int_poly [simp]: 
+  "algebraic x \<Longrightarrow> ipoly (min_int_poly x) (x :: 'a :: {field_gcd, field_char_0}) = 0"
+  using min_int_poly_represents[of x] by (auto simp: represents_def)
+
+lemma min_int_poly_nonzero [simp]:
+  fixes x :: "'a :: {field_char_0, field_gcd}"
+  shows "min_int_poly x \<noteq> 0"
+  using lead_coeff_min_int_poly_pos[of x] by auto
+
+lemma min_int_poly_normalize [simp]:
+  fixes x :: "'a :: {field_char_0, field_gcd}"
+  shows "normalize (min_int_poly x) = min_int_poly x"
+  unfolding normalize_poly_def using lead_coeff_min_int_poly_pos[of x] by simp
+
+lemma min_int_poly_prime_elem [intro]:
+  fixes x :: "'a :: {field_char_0, field_gcd}"
+  shows "prime_elem (min_int_poly x)"
+  using min_int_poly_irreducible[of x] by blast
+
+lemma min_int_poly_prime [intro]:
+  fixes x :: "'a :: {field_char_0, field_gcd}"
+  shows "prime (min_int_poly x)"
+  using min_int_poly_prime_elem[of x]
+  by (simp only: prime_normalize_iff [symmetric] min_int_poly_normalize)
+
+lemma min_int_poly_unique:
+  fixes x :: "'a :: {field_char_0, field_gcd}"
+  assumes "p represents x" "irreducible p" "Polynomial.lead_coeff p > 0"
+  shows "min_int_poly x = p"
+proof -
+  from assms(1) have x: "algebraic x"
+    using algebraic_iff_represents by blast
+  thus ?thesis
+    using the1_equality[OF algebraic_imp_represents_unique[OF x], of p] assms
+    unfolding min_int_poly_def by auto
+qed
+
+lemma min_int_poly_of_int [simp]:
+  "min_int_poly (of_int n :: 'a :: {field_char_0, field_gcd}) = [:-of_int n, 1:]"
+  by (intro min_int_poly_unique irreducible_linear_poly) auto
+
+lemma min_int_poly_of_nat [simp]:
+  "min_int_poly (of_nat n :: 'a :: {field_char_0, field_gcd}) = [:-of_nat n, 1:]"
+  using min_int_poly_of_int[of "int n"] by (simp del: min_int_poly_of_int)
+
+lemma min_int_poly_0 [simp]: "min_int_poly (0 :: 'a :: {field_char_0, field_gcd}) = [:0, 1:]"
+  using min_int_poly_of_int[of 0] unfolding of_int_0 by simp
+
+lemma min_int_poly_1 [simp]: "min_int_poly (1 :: 'a :: {field_char_0, field_gcd}) = [:-1, 1:]"
+  using min_int_poly_of_int[of 1] unfolding of_int_1 by simp
+
+lemma poly_min_int_poly_0_eq_0_iff [simp]:
+  fixes x :: "'a :: {field_char_0, field_gcd}"
+  assumes "algebraic x"
+  shows "poly (min_int_poly x) 0 = 0 \<longleftrightarrow> x = 0"
+proof
+  assume *: "poly (min_int_poly x) 0 = 0"
+  show "x = 0"
+  proof (rule ccontr)
+    assume "x \<noteq> 0"
+    hence "poly (min_int_poly x) 0 \<noteq> 0"
+      using assms by (intro represents_irr_non_0) auto
+    with * show False by contradiction
+  qed
+qed auto
+
+lemma min_int_poly_conv_Gcd:
+  fixes x :: "'a :: {field_char_0, field_gcd}"
+  assumes "algebraic x"
+  shows "min_int_poly x = Gcd {p. p \<noteq> 0 \<and> p represents x}"
+proof (rule sym, rule Gcd_eqI, (safe)?)
+  fix p assume p: "\<And>q. q \<in> {p. p \<noteq> 0 \<and> p represents x} \<Longrightarrow> p dvd q"
+  show "p dvd min_int_poly x"
+    using assms by (intro p) auto
+next
+  fix p assume p: "p \<noteq> 0" "p represents x"
+  have "min_int_poly x represents x"
+    using assms by auto
+  hence "poly (gcd (of_int_poly (min_int_poly x)) (of_int_poly p)) x = 0"
+    using p by (intro poly_gcd_eq_0I) auto
+  hence "ipoly (gcd (min_int_poly x) p) x = 0"
+    by (subst (asm) gcd_of_int_poly) auto
+  hence "gcd (min_int_poly x) p represents x"
+    using p unfolding represents_def by auto
+
+  have "min_int_poly x dvd gcd (min_int_poly x) p \<or> is_unit (gcd (min_int_poly x) p)"
+    by (intro irreducibleD') auto
+  moreover from \<open>gcd (min_int_poly x) p represents x\<close> have "\<not>is_unit (gcd (min_int_poly x) p)"
+    by (auto simp: represents_def)
+  ultimately have "min_int_poly x dvd gcd (min_int_poly x) p"
+    by blast
+  also have "\<dots> dvd p"
+    by blast
+  finally show "min_int_poly x dvd p" .
+qed auto
+
+lemma min_int_poly_eqI:
+  fixes x :: "'a :: {field_char_0, field_gcd}"
+  assumes "p represents x" "irreducible p" "Polynomial.lead_coeff p \<ge> 0"
+  shows   "min_int_poly x = p"
+proof -
+  from assms have [simp]: "p \<noteq> 0"
+    by auto
+  have "Polynomial.lead_coeff p \<noteq> 0"
+    by auto
+  with assms(3) have "Polynomial.lead_coeff p > 0"
+    by linarith
+  moreover have "algebraic x"
+    using \<open>p represents x\<close> by (meson algebraic_iff_represents)
+  ultimately show ?thesis
+    unfolding min_int_poly_def
+    using the1_equality[OF algebraic_imp_represents_unique[OF \<open>algebraic x\<close>], of p] assms by auto
+qed
+
+end
\ No newline at end of file
diff --git a/thys/Hermite_Lindemann/Misc_HLW.thy b/thys/Hermite_Lindemann/Misc_HLW.thy
new file mode 100644
--- /dev/null
+++ b/thys/Hermite_Lindemann/Misc_HLW.thy
@@ -0,0 +1,231 @@
+(*
+  File:     Misc_HLW.thy
+  Author:   Manuel Eberl, TU München
+*)
+section \<open>Miscellaneous facts\<close>
+theory Misc_HLW
+imports
+  Complex_Main
+  "HOL-Library.Multiset"
+  "HOL-Library.Permutations"
+  "HOL-Library.FuncSet"
+  "HOL-Library.Groups_Big_Fun"
+  "HOL-Library.Poly_Mapping"
+  "HOL-Library.Landau_Symbols"
+  "HOL-Computational_Algebra.Computational_Algebra"
+begin
+
+lemma set_mset_subset_singletonD:
+  assumes "set_mset A \<subseteq> {x}"
+  shows   "A = replicate_mset (size A) x"
+  using assms by (induction A) auto
+  
+lemma image_mset_eq_replicate_msetD:
+  assumes "image_mset f A = replicate_mset n y"
+  shows   "\<forall>x\<in>#A. f x = y"
+proof -
+  have "f ` set_mset A = set_mset (image_mset f A)"
+    by simp
+  also note assms
+  finally show ?thesis by (auto split: if_splits)
+qed
+
+lemma bij_betw_permutes_compose_left:
+  assumes "\<pi> permutes A"
+  shows   "bij_betw (\<lambda>\<sigma>. \<pi> \<circ> \<sigma>) {\<sigma>. \<sigma> permutes A} {\<sigma>. \<sigma> permutes A}"
+proof (rule bij_betwI)
+  show "(\<circ>) \<pi> \<in> {\<sigma>. \<sigma> permutes A} \<rightarrow> {\<sigma>. \<sigma> permutes A}"
+    by (auto intro: permutes_compose assms)
+  show "(\<circ>) (inv_into UNIV \<pi>) \<in> {\<sigma>. \<sigma> permutes A} \<rightarrow> {\<sigma>. \<sigma> permutes A}"
+    by (auto intro: permutes_compose assms permutes_inv)
+qed (use permutes_inverses[OF assms] in auto)
+
+lemma bij_betw_compose_left_perm_Pi:
+  assumes "\<pi> permutes B"
+  shows   "bij_betw (\<lambda>f. (\<pi> \<circ> f)) (A \<rightarrow> B) (A \<rightarrow> B)"
+proof (rule bij_betwI)
+  have *: "(\<lambda>f. (\<pi> \<circ> f)) \<in> (A \<rightarrow> B) \<rightarrow> A \<rightarrow> B" if \<pi>: "\<pi> permutes B" for \<pi>
+    by (auto simp: permutes_in_image[OF \<pi>])
+  show "(\<lambda>f. (\<pi> \<circ> f)) \<in> (A \<rightarrow> B) \<rightarrow> A \<rightarrow> B"
+    by (rule *) fact
+  show "(\<lambda>f. (inv_into UNIV \<pi> \<circ> f)) \<in> (A \<rightarrow> B) \<rightarrow> A \<rightarrow> B"
+    by (intro * permutes_inv) fact
+qed (auto simp: permutes_inverses[OF assms] fun_eq_iff)
+
+lemma bij_betw_compose_left_perm_PiE:
+  assumes "\<pi> permutes B"
+  shows   "bij_betw (\<lambda>f. restrict (\<pi> \<circ> f) A) (A \<rightarrow>\<^sub>E B) (A \<rightarrow>\<^sub>E B)"
+proof (rule bij_betwI)
+  have *: "(\<lambda>f. restrict (\<pi> \<circ> f) A) \<in> (A \<rightarrow>\<^sub>E B) \<rightarrow> A \<rightarrow>\<^sub>E B" if \<pi>: "\<pi> permutes B" for \<pi>
+    by (auto simp: permutes_in_image[OF \<pi>])
+  show "(\<lambda>f. restrict (\<pi> \<circ> f) A) \<in> (A \<rightarrow>\<^sub>E B) \<rightarrow> A \<rightarrow>\<^sub>E B"
+    by (rule *) fact
+  show "(\<lambda>f. restrict (inv_into UNIV \<pi> \<circ> f) A) \<in> (A \<rightarrow>\<^sub>E B) \<rightarrow> A \<rightarrow>\<^sub>E B"
+    by (intro * permutes_inv) fact
+qed (auto simp: permutes_inverses[OF assms] fun_eq_iff)
+
+lemma bij_betw_image_mset_set:
+  assumes "bij_betw f A B"
+  shows   "image_mset f (mset_set A) = mset_set B"
+  using assms by (simp add: bij_betw_def image_mset_mset_set)
+
+lemma finite_multisets_of_size:
+  assumes "finite A"
+  shows   "finite {X. set_mset X \<subseteq> A \<and> size X = n}"
+proof (rule finite_subset)
+  show "{X. set_mset X \<subseteq> A \<and> size X = n} \<subseteq> mset ` {xs. set xs \<subseteq> A \<and> length xs = n}"
+  proof
+    fix X assume X: "X \<in> {X. set_mset X \<subseteq> A \<and> size X = n}"
+    obtain xs where [simp]: "X = mset xs"
+      by (metis ex_mset)
+    thus "X \<in> mset ` {xs. set xs \<subseteq> A \<and> length xs = n}"
+      using X by auto
+  qed
+next
+  show "finite (mset ` {xs. set xs \<subseteq> A \<and> length xs = n})"
+    by (intro finite_imageI finite_lists_length_eq assms)
+qed
+
+lemma sum_mset_image_mset_sum_mset_image_mset:
+   "sum_mset (image_mset g (sum_mset (image_mset f A))) =
+    sum_mset (image_mset (\<lambda>x. sum_mset (image_mset g (f x))) A)"
+  by (induction A) auto
+
+lemma sum_mset_image_mset_singleton: "sum_mset (image_mset (\<lambda>x. {#f x#}) A) = image_mset f A"
+  by (induction A) auto
+
+lemma sum_mset_conv_sum:
+  "sum_mset (image_mset f A) = (\<Sum>x\<in>set_mset A. of_nat (count A x) * f x)"
+proof (induction A rule: full_multiset_induct)
+  case (less A)
+  show ?case
+  proof (cases "A = {#}")
+    case False
+    then obtain x where x: "x \<in># A"
+      by auto
+    define n where "n = count A x"
+    define A' where "A' = filter_mset (\<lambda>y. y \<noteq> x) A"
+    have A_eq: "A = replicate_mset n x + A'"
+      by (intro multiset_eqI) (auto simp: A'_def n_def)
+    have [simp]: "x \<notin># A'" "count A' x = 0"
+      by (auto simp: A'_def)
+    have "n \<noteq> 0"
+      using x by (auto simp: n_def)
+    
+    have "sum_mset (image_mset f A) = of_nat n * f x + sum_mset (image_mset f A')"
+      by (simp add: A_eq)
+    also have "A' \<subset># A"
+      unfolding A'_def using x by (simp add: filter_mset_eq_conv subset_mset_def)
+    with less.IH have "sum_mset (image_mset f A') = (\<Sum>x\<in>set_mset A'. of_nat (count A' x) * f x)"
+      by simp
+    also have "\<dots> = (\<Sum>x\<in>set_mset A'. of_nat (count A x) * f x)"
+      by (intro sum.cong) (auto simp: A_eq)
+    also have "of_nat n * f x + \<dots> = (\<Sum>x\<in>insert x (set_mset A'). of_nat (count A x) * f x)"
+      by (subst sum.insert) (auto simp: A_eq)
+    also from \<open>n \<noteq> 0\<close> have "insert x (set_mset A') = set_mset A"
+      by (auto simp: A_eq)
+    finally show ?thesis .
+  qed auto
+qed
+
+lemma sum_mset_conv_Sum_any:
+  "sum_mset (image_mset f A) = Sum_any (\<lambda>x. of_nat (count A x) * f x)"
+proof -
+  have "sum_mset (image_mset f A) = (\<Sum>x\<in>set_mset A. of_nat (count A x) * f x)"
+    by (rule sum_mset_conv_sum)
+  also have "\<dots> = Sum_any (\<lambda>x. of_nat (count A x) * f x)"
+  proof (rule Sum_any.expand_superset [symmetric])
+    show "{x. of_nat (count A x) * f x \<noteq> 0} \<subseteq> set_mset A"
+    proof
+      fix x assume "x \<in> {x. of_nat (count A x) * f x \<noteq> 0}"
+      hence "count A x \<noteq> 0"
+        by (intro notI) auto
+      thus "x \<in># A"
+        by auto
+    qed
+  qed auto
+  finally show ?thesis .
+qed
+
+lemma Sum_any_sum_swap:
+  assumes "finite A" "\<And>y. finite {x. f x y \<noteq> 0}"
+  shows   "Sum_any (\<lambda>x. sum (f x) A) = (\<Sum>y\<in>A. Sum_any (\<lambda>x. f x y))"
+proof -
+  have "Sum_any (\<lambda>x. sum (f x) A) = Sum_any (\<lambda>x. Sum_any (\<lambda>y. f x y when y \<in> A))"
+    unfolding when_def by (subst Sum_any.conditionalize) (use assms in simp_all)
+  also have "\<dots> = Sum_any (\<lambda>y. Sum_any (\<lambda>x. f x y when y \<in> A))"
+    by (intro Sum_any.swap[of "(\<Union>y\<in>A. {x. f x y \<noteq> 0}) \<times> A"] finite_SigmaI finite_UN_I assms) auto
+  also have "(\<lambda>y. Sum_any (\<lambda>x. f x y when y \<in> A)) = (\<lambda>y. Sum_any (\<lambda>x. f x y) when y \<in> A)"
+    by (auto simp: when_def)
+  also have "Sum_any \<dots> = (\<Sum>y\<in>A. Sum_any (\<lambda>x. f x y))"
+    unfolding when_def by (subst Sum_any.conditionalize) (use assms in simp_all)
+  finally show ?thesis .
+qed
+
+lemma (in landau_pair) big_power:
+  assumes "f \<in> L F g"
+  shows   "(\<lambda>x. f x ^ n) \<in> L F (\<lambda>x. g x ^ n)"
+  using big_prod[of "{..<n}" "\<lambda>_. f" F "\<lambda>_. g"] assms by simp
+
+lemma (in landau_pair) small_power:
+  assumes "f \<in> l F g" "n > 0"
+  shows   "(\<lambda>x. f x ^ n) \<in> l F (\<lambda>x. g x ^ n)"
+  using assms(2,1)
+  by (induction rule: nat_induct_non_zero) (auto intro!: small.mult)
+
+lemma pairwise_imp_disjoint_family_on:
+  assumes "pairwise R A"
+  assumes "\<And>m n. m \<in> A \<Longrightarrow> n \<in> A \<Longrightarrow> R m n \<Longrightarrow> f m \<inter> f n = {}"
+  shows   "disjoint_family_on f A"
+  using assms
+  unfolding disjoint_family_on_def pairwise_def by blast
+
+lemma (in comm_monoid_set) If_eq:
+  assumes "y \<in> A" "finite A"
+  shows   "F (\<lambda>x. g x (if x = y then h1 x else h2 x)) A = f (g y (h1 y)) (F (\<lambda>x. g x (h2 x)) (A-{y}))"
+proof -
+  have "F (\<lambda>x. g x (if x = y then h1 x else h2 x)) A =
+          f (g y (h1 y)) (F (\<lambda>x. g x (if x = y then h1 x else h2 x)) (A-{y}))"
+    using assms by (subst remove[of _ y]) auto
+  also have "F (\<lambda>x. g x (if x = y then h1 x else h2 x)) (A-{y}) = F (\<lambda>x. g x (h2 x)) (A-{y})"
+    by (intro cong) auto
+  finally show ?thesis by simp
+qed
+
+lemma prod_nonzeroI:
+  fixes f :: "'a \<Rightarrow> 'b :: {semiring_no_zero_divisors, comm_semiring_1}"
+  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0"
+  shows "prod f A \<noteq> 0"
+  using assms by (induction rule: infinite_finite_induct) auto
+
+lemma frequently_prime_cofinite: "frequently (prime :: nat \<Rightarrow> bool) cofinite"
+  unfolding INFM_nat_le by (meson bigger_prime less_imp_le)
+
+lemma frequently_eventually_mono:
+  assumes "frequently Q F" "eventually P F" "\<And>x. P x \<Longrightarrow> Q x \<Longrightarrow> R x"
+  shows   "frequently R F"
+proof (rule frequently_mp[OF _ assms(1)])
+  show "eventually (\<lambda>x. Q x \<longrightarrow> R x) F"
+    using assms(2) by eventually_elim (use assms(3) in blast)
+qed
+
+lemma bij_betw_Diff:
+  assumes "bij_betw f A B" "bij_betw f A' B'" "A' \<subseteq> A" "B' \<subseteq> B"
+  shows   "bij_betw f (A - A') (B - B')"
+  unfolding bij_betw_def
+proof
+  have "inj_on f A"
+    using assms(1) by (auto simp: bij_betw_def)
+  thus "inj_on f (A - A')"
+    by (rule inj_on_subset) auto
+  have "f ` (A - A') = f ` A - f ` A'"
+    by (intro inj_on_image_set_diff[OF \<open>inj_on f A\<close>]) (use \<open>A' \<subseteq> A\<close> in auto)
+  also have "\<dots> = B - B'"
+    using assms(1,2) by (auto simp: bij_betw_def)
+  finally show "f` (A - A') = B - B'" .
+qed
+    
+lemma bij_betw_singleton: "bij_betw f {x} {y} \<longleftrightarrow> f x = y"
+  by (auto simp: bij_betw_def)
+
+end
\ No newline at end of file
diff --git a/thys/Hermite_Lindemann/More_Algebraic_Numbers_HLW.thy b/thys/Hermite_Lindemann/More_Algebraic_Numbers_HLW.thy
new file mode 100644
--- /dev/null
+++ b/thys/Hermite_Lindemann/More_Algebraic_Numbers_HLW.thy
@@ -0,0 +1,245 @@
+(*
+  File:     More_Algebraic_Numbers_HLW.thy
+  Author:   Manuel Eberl, TU München
+*)
+section \<open>More facts about algebraic numbers\<close>
+theory More_Algebraic_Numbers_HLW
+  imports "Algebraic_Numbers.Algebraic_Numbers"
+begin
+
+subsection \<open>Miscellaneous\<close>
+
+(* TODO: Move! All of this belongs in Algebraic_Numbers *)
+
+lemma in_Ints_imp_algebraic [simp, intro]: "x \<in> \<int> \<Longrightarrow> algebraic x"
+  by (intro algebraic_int_imp_algebraic int_imp_algebraic_int)
+
+lemma in_Rats_imp_algebraic [simp, intro]: "x \<in> \<rat> \<Longrightarrow> algebraic x"
+  by (auto elim!: Rats_cases' intro: algebraic_div)
+
+lemma algebraic_uminus_iff [simp]: "algebraic (-x) \<longleftrightarrow> algebraic x"
+  using algebraic_uminus[of x] algebraic_uminus[of "-x"] by auto
+
+lemma algebraic_0 [simp]: "algebraic (0 :: 'a :: field_char_0)"
+  and algebraic_1 [simp]: "algebraic (1 :: 'a :: field_char_0)"
+  by auto  
+
+lemma algebraic_sum [intro]:
+  "(\<And>x. x \<in> A \<Longrightarrow> algebraic (f x)) \<Longrightarrow> algebraic (sum f A)"
+  by (induction A rule: infinite_finite_induct) (auto intro!: algebraic_plus)
+
+lemma algebraic_prod [intro]:
+  "(\<And>x. x \<in> A \<Longrightarrow> algebraic (f x)) \<Longrightarrow> algebraic (prod f A)"
+  by (induction A rule: infinite_finite_induct) (auto intro!: algebraic_times)
+
+lemma algebraic_sum_list [intro]:
+  "(\<And>x. x \<in> set xs \<Longrightarrow> algebraic x) \<Longrightarrow> algebraic (sum_list xs)"
+  by (induction xs) (auto intro!: algebraic_plus)
+
+lemma algebraic_prod_list [intro]:
+  "(\<And>x. x \<in> set xs \<Longrightarrow> algebraic x) \<Longrightarrow> algebraic (prod_list xs)"
+  by (induction xs) (auto intro!: algebraic_times)
+
+lemma algebraic_sum_mset [intro]:
+  "(\<And>x. x \<in># A \<Longrightarrow> algebraic x) \<Longrightarrow> algebraic (sum_mset A)"
+  by (induction A) (auto intro!: algebraic_plus)
+
+lemma algebraic_prod_mset [intro]:
+  "(\<And>x. x \<in># A \<Longrightarrow> algebraic x) \<Longrightarrow> algebraic (prod_mset A)"
+  by (induction A) (auto intro!: algebraic_times)
+
+lemma algebraic_power [intro]: "algebraic x \<Longrightarrow> algebraic (x ^ n)"
+  by (induction n) (auto intro: algebraic_times)
+
+lemma algebraic_csqrt [intro]: "algebraic x \<Longrightarrow> algebraic (csqrt x)"
+  by (rule algebraic_nth_root[of 2 x]) auto
+
+lemma algebraic_csqrt_iff [simp]: "algebraic (csqrt x) \<longleftrightarrow> algebraic x"
+proof
+  assume "algebraic (csqrt x)"
+  hence "algebraic (csqrt x ^ 2)"
+    by (rule algebraic_power)
+  also have "csqrt x ^ 2 = x"
+    by simp
+  finally show "algebraic x" .
+qed auto
+
+lemmas [intro] = algebraic_plus algebraic_times algebraic_uminus algebraic_div
+
+lemma algebraic_power_iff [simp]:
+  assumes "n > 0"
+  shows   "algebraic (x ^ n) \<longleftrightarrow> algebraic x"
+  using algebraic_nth_root[of n "x ^ n" x] assms by auto
+
+lemma algebraic_ii [simp]: "algebraic \<i>"
+  by (intro algebraic_int_imp_algebraic) auto
+
+lemma algebraic_int_fact [simp, intro]: "algebraic_int (fact n)"
+  by (intro int_imp_algebraic_int fact_in_Ints)
+
+lemma algebraic_minus [intro]: "algebraic x \<Longrightarrow> algebraic y \<Longrightarrow> algebraic (x - y)"
+  using algebraic_plus[of x "-y"] by simp
+
+lemma algebraic_add_cancel_left [simp]:
+  assumes "algebraic x"
+  shows   "algebraic (x + y) \<longleftrightarrow> algebraic y"
+proof
+  assume "algebraic (x + y)"
+  hence "algebraic (x + y - x)"
+    using assms by (intro algebraic_minus) auto
+  thus "algebraic y" by simp
+qed (auto intro: algebraic_plus assms)
+
+lemma algebraic_add_cancel_right [simp]:
+  assumes "algebraic y"
+  shows   "algebraic (x + y) \<longleftrightarrow> algebraic x"
+  using algebraic_add_cancel_left[of y x] assms
+  by (simp add: add.commute del: algebraic_add_cancel_left)
+
+lemma algebraic_diff_cancel_left [simp]:
+  assumes "algebraic x"
+  shows   "algebraic (x - y) \<longleftrightarrow> algebraic y"
+  using algebraic_add_cancel_left[of x "-y"] assms by (simp del: algebraic_add_cancel_left)
+
+lemma algebraic_diff_cancel_right [simp]:
+  assumes "algebraic y"
+  shows   "algebraic (x - y) \<longleftrightarrow> algebraic x"
+  using algebraic_add_cancel_right[of "-y" x] assms by (simp del: algebraic_add_cancel_right)
+
+lemma algebraic_mult_cancel_left [simp]:
+  assumes "algebraic x" "x \<noteq> 0"
+  shows   "algebraic (x * y) \<longleftrightarrow> algebraic y"
+proof
+  assume "algebraic (x * y)"
+  hence "algebraic (x * y / x)"
+    using assms by (intro algebraic_div) auto
+  also have "x * y / x = y"
+    using assms by auto
+  finally show "algebraic y" .
+qed (auto intro: algebraic_times assms)
+
+lemma algebraic_mult_cancel_right [simp]:
+  assumes "algebraic y" "y \<noteq> 0"
+  shows   "algebraic (x * y) \<longleftrightarrow> algebraic x"
+  using algebraic_mult_cancel_left[of y x] assms
+  by (simp add: mult.commute del: algebraic_mult_cancel_left)
+
+lemma algebraic_inverse_iff [simp]: "algebraic (inverse y) \<longleftrightarrow> algebraic y"
+proof
+  assume "algebraic (inverse y)"
+  hence "algebraic (inverse (inverse y))"
+    by (rule algebraic_inverse)
+  thus "algebraic y" by simp
+qed (auto intro: algebraic_inverse)
+
+lemma algebraic_divide_cancel_left [simp]:
+  assumes "algebraic x" "x \<noteq> 0"
+  shows   "algebraic (x / y) \<longleftrightarrow> algebraic y"
+proof -
+  have "algebraic (x * inverse y) \<longleftrightarrow> algebraic (inverse y)"
+    by (intro algebraic_mult_cancel_left assms)
+  also have "\<dots> \<longleftrightarrow> algebraic y"
+    by (intro algebraic_inverse_iff)
+  finally show ?thesis by (simp add: field_simps)
+qed
+
+lemma algebraic_divide_cancel_right [simp]:
+  assumes "algebraic y" "y \<noteq> 0"
+  shows   "algebraic (x / y) \<longleftrightarrow> algebraic x"
+proof -
+  have "algebraic (x * inverse y) \<longleftrightarrow> algebraic x"
+    using assms by (intro algebraic_mult_cancel_right) auto
+  thus ?thesis by (simp add: field_simps)
+qed
+
+
+subsection \<open>Turning an algebraic number into an algebraic integer\<close>
+
+subsection \<open>
+  Multiplying an algebraic number with a suitable integer turns it into an algebraic integer.
+\<close>
+
+lemma algebraic_imp_algebraic_int:
+  fixes x :: "'a :: field_char_0"
+  assumes "ipoly p x = 0" "p \<noteq> 0"
+  defines "c \<equiv> Polynomial.lead_coeff p"
+  shows   "algebraic_int (of_int c * x)"
+proof -
+  define n where "n = Polynomial.degree p"
+  define p' where "p' = Abs_poly (\<lambda>i. if i = n then 1 else c ^ (n - i - 1) * poly.coeff p i)"
+  have "n > 0"
+    using assms unfolding n_def by (intro Nat.gr0I) (auto elim!: degree_eq_zeroE)
+
+  have coeff_p': "poly.coeff p' i =
+                    (if i = n then 1 else c ^ (n - i - 1) * poly.coeff p i)"
+    (is "_ = ?f i") for i unfolding p'_def
+  proof (subst poly.Abs_poly_inverse)
+    have "eventually (\<lambda>i. poly.coeff p i = 0) cofinite"
+      using MOST_coeff_eq_0 by blast
+    hence "eventually (\<lambda>i. ?f i = 0) cofinite"
+      by eventually_elim (use assms in \<open>auto simp: n_def\<close>)
+    thus "?f \<in> {f. eventually (\<lambda>i. f i = 0) cofinite}" by simp
+  qed auto
+
+  have deg_p': "Polynomial.degree p' = n"
+  proof -
+    from assms have "(\<lambda>n. \<forall>i>n. poly.coeff p' i = 0) = (\<lambda>n. \<forall>i>n. poly.coeff p i = 0)"
+      by (auto simp: coeff_p' fun_eq_iff n_def)
+    thus ?thesis
+      by (simp add: Polynomial.degree_def n_def)
+  qed
+
+  have lead_coeff_p': "Polynomial.lead_coeff p' = 1"
+    by (simp add: coeff_p' deg_p')
+
+  have "0 = of_int (c ^ (n - 1)) * (\<Sum>i\<le>n. of_int (poly.coeff p i) * x ^ i)"
+    using assms unfolding n_def poly_altdef by simp
+  also have "\<dots> = (\<Sum>i\<le>n. of_int (c ^ (n - 1) * poly.coeff p i) * x ^ i)"
+    by (simp add: sum_distrib_left sum_distrib_right mult_ac)
+  also have "\<dots> = (\<Sum>i\<le>n. of_int (poly.coeff p' i) * (of_int c * x) ^ i)"
+  proof (intro sum.cong, goal_cases)
+    case (2 i)
+    have "of_int (poly.coeff p' i) * (of_int c * x) ^ i =
+          of_int (c ^ i * poly.coeff p' i) * x ^ i"
+      by (simp add: algebra_simps)
+    also have "c ^ i * poly.coeff p' i = c ^ (n - 1) * poly.coeff p i"
+    proof (cases "i = n")
+      case True
+      hence "c ^ i * poly.coeff p' i = c ^ n"
+        by (auto simp: coeff_p' simp flip: power_Suc)
+      also have "n = Suc (n - 1)"
+        using \<open>n > 0\<close> by simp
+      also have "c ^ \<dots> = c * c ^ (n - 1)"
+        by simp
+      finally show ?thesis
+        using True by (simp add: c_def n_def)
+    next
+      case False
+      thus ?thesis using 2
+        by (auto simp: coeff_p' simp flip: power_add)
+    qed
+    finally show ?case ..
+  qed auto
+  also have "\<dots> = ipoly p' (of_int c * x)"
+    by (simp add: poly_altdef n_def deg_p')
+  finally have "ipoly p' (of_int c * x) = 0" ..
+
+  with lead_coeff_p' show ?thesis
+    unfolding algebraic_int_altdef_ipoly by blast
+qed
+
+lemma algebraic_imp_algebraic_int':
+  fixes x :: "'a :: field_char_0"
+  assumes "ipoly p x = 0" "p \<noteq> 0" "Polynomial.lead_coeff p dvd c"
+  shows   "algebraic_int (of_int c * x)"
+proof -
+  from assms(3) obtain c' where c_eq: "c = Polynomial.lead_coeff p * c'"
+    by auto
+  have "algebraic_int (of_int c' * (of_int (Polynomial.lead_coeff p) * x))"
+    by (rule algebraic_int_times[OF _ algebraic_imp_algebraic_int]) (use assms in auto)
+  also have "of_int c' * (of_int (Polynomial.lead_coeff p) * x) = of_int c * x"
+    by (simp add: c_eq mult_ac)
+  finally show ?thesis .
+qed
+
+end
\ No newline at end of file
diff --git a/thys/Hermite_Lindemann/More_Multivariate_Polynomial_HLW.thy b/thys/Hermite_Lindemann/More_Multivariate_Polynomial_HLW.thy
new file mode 100644
--- /dev/null
+++ b/thys/Hermite_Lindemann/More_Multivariate_Polynomial_HLW.thy
@@ -0,0 +1,202 @@
+(*
+  File:     More_Multivariate_Polynomial_HLW.thy
+  Author:   Manuel Eberl, TU München
+*)
+section \<open>Additional facts about multivariate polynomials\<close>
+theory More_Multivariate_Polynomial_HLW
+  imports "Power_Sum_Polynomials.Power_Sum_Polynomials_Library"
+begin
+
+subsection \<open>Miscellaneous\<close>
+
+lemma Var_altdef: "Var i = monom (Poly_Mapping.single i 1) 1"
+  by transfer' (simp add: Var\<^sub>0_def)
+
+lemma Const_conv_monom: "Const c = monom 0 c"
+  by transfer' (auto simp: Const\<^sub>0_def)
+
+lemma smult_conv_mult_Const: "smult c p = Const c * p"
+  by (simp add: smult_conv_mult Const_conv_monom)
+
+lemma mpoly_map_vars_Var [simp]: "bij f \<Longrightarrow> mpoly_map_vars f (Var i) = Var (f i)"
+  unfolding Var_altdef
+  by (subst mpoly_map_vars_monom) (auto simp: permutep_single bij_imp_bij_inv inv_inv_eq)
+
+lemma symmetric_mpoly_symmetric_prod':
+  assumes "\<And>\<pi>. \<pi> permutes A \<Longrightarrow> g \<pi> permutes X"
+  assumes "\<And>x \<pi>. x \<in> X \<Longrightarrow> \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> (f x) = f (g \<pi> x)"
+  shows "symmetric_mpoly A (\<Prod>x\<in>X. f x)"
+  unfolding symmetric_mpoly_def
+proof safe
+  fix \<pi> assume \<pi>: "\<pi> permutes A"
+  have "mpoly_map_vars \<pi> (prod f X) = (\<Prod>x\<in>X. mpoly_map_vars \<pi> (f x))"
+    by simp
+  also have "\<dots> = (\<Prod>x\<in>X. f (g \<pi> x))"
+    by (intro prod.cong assms \<pi> refl)
+  also have "\<dots> = (\<Prod>x\<in>g \<pi>`X. f x)"
+    using assms(1)[OF \<pi>] by (subst prod.reindex) (auto simp: permutes_inj_on)
+  also have "g \<pi> ` X = X"
+    using assms(1)[OF \<pi>] by (simp add: permutes_image)
+  finally show "mpoly_map_vars \<pi> (prod f X) = prod f X" .
+qed
+
+
+
+subsection \<open>Converting a univariate polynomial into a multivariate one\<close>
+
+lift_definition mpoly_of_poly_aux :: "nat \<Rightarrow> 'a :: zero poly \<Rightarrow> (nat \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 'a" is
+  "\<lambda>i c m. if Poly_Mapping.keys m \<subseteq> {i} then c (Poly_Mapping.lookup m i) else 0"
+proof goal_cases
+  case (1 i c)
+  hence fin: "finite {n. c n \<noteq> 0}"
+    by (metis eventually_cofinite)
+  show "finite {x. (if keys x \<subseteq> {i} then c (lookup x i) else 0) \<noteq> 0}"
+  proof (rule finite_subset)
+    show "finite (Poly_Mapping.single i ` {n. c n \<noteq> 0})"
+      by (intro finite_imageI fin)
+  next
+    show "{x. (if keys x \<subseteq> {i} then c (lookup x i) else 0) \<noteq> 0} \<subseteq>
+            Poly_Mapping.single i ` {n. c n \<noteq> 0}"
+    proof (safe, split if_splits)
+      fix x :: "(nat \<Rightarrow>\<^sub>0 nat)"
+      assume x: "keys x \<subseteq> {i}" "c (lookup x i) \<noteq> 0"
+      hence "x = Poly_Mapping.single i (lookup x i)"
+        by (metis Diff_eq_empty_iff keys_empty_iff lookup_single_eq
+                  remove_key_keys remove_key_single remove_key_sum)
+      thus "x \<in> Poly_Mapping.single i ` {n. c n \<noteq> 0}"
+        using x by blast
+    qed auto
+  qed
+qed
+
+lift_definition mpoly_of_poly :: "nat \<Rightarrow> 'a :: zero poly \<Rightarrow> 'a mpoly" is
+  "mpoly_of_poly_aux" .
+
+lemma mpoly_of_poly_0 [simp]: "mpoly_of_poly i 0 = 0"
+  by (transfer', transfer) auto
+
+lemma coeff_mpoly_of_poly1 [simp]:
+  "coeff (mpoly_of_poly i p) (Poly_Mapping.single i n) = poly.coeff p n"
+  by (transfer', transfer') auto
+
+lemma coeff_mpoly_of_poly2 [simp]:
+  assumes "\<not>keys x \<subseteq> {i}"
+  shows "coeff (mpoly_of_poly i p) x = 0"
+  using assms by (transfer', transfer') auto
+
+lemma coeff_mpoly_of_poly:
+  "coeff (mpoly_of_poly i p) m =
+     (poly.coeff p (Poly_Mapping.lookup m i) when keys m \<subseteq> {i})"
+  by (transfer', transfer') auto
+
+lemma poly_mapping_single_eq_0_iff [simp]: "Poly_Mapping.single i n = 0 \<longleftrightarrow> n = 0"
+  by (metis lookup_single_eq single_zero)
+
+lemma mpoly_of_poly_pCons [simp]:
+  fixes p :: "'a :: semiring_1 poly"
+  shows "mpoly_of_poly i (pCons c p) = Const c + Var i * mpoly_of_poly i p"
+proof (rule mpoly_eqI)
+  fix mon :: "nat \<Rightarrow>\<^sub>0 nat"
+  define moni :: "nat \<Rightarrow>\<^sub>0 nat" where "moni = Poly_Mapping.single i 1"
+  have "coeff (Var i * mpoly_of_poly i p) mon =
+          (\<Sum>l. (1 when l = moni) * (\<Sum>q. coeff (mpoly_of_poly i p) q when mon = moni + q))"
+    unfolding coeff_mpoly_times prod_fun_def coeff_Var moni_def
+    by (rule Sum_any.cong) (auto simp: when_def)
+  also have "\<dots> = (\<Sum>a. coeff (mpoly_of_poly i p) a when mon = moni + a)"
+    by (subst Sum_any_left_distrib [symmetric]) simp_all
+  finally have eq: "coeff (Var i * mpoly_of_poly i p) mon = \<dots>" .
+
+  show "coeff (mpoly_of_poly i (pCons c p)) mon = coeff (Const c + Var i * mpoly_of_poly i p) mon"
+  proof (cases "keys mon \<subseteq> {i}")
+    case False
+    hence [simp]: "mon \<noteq> 0"
+      by auto
+    obtain j where j: "j \<in> keys mon" "j \<noteq> i"
+      using False by auto
+    have "coeff (mpoly_of_poly i p) mon' = 0" if mon_eq: "mon = moni + mon'" for mon'
+    proof -
+      have "Poly_Mapping.lookup mon j \<noteq> 0"
+        using j by (meson lookup_eq_zero_in_keys_contradict)
+      also have "Poly_Mapping.lookup mon j = Poly_Mapping.lookup mon' j"
+        unfolding mon_eq moni_def using j by (simp add: lookup_add lookup_single)
+      finally have "j \<in> keys mon'"
+        by (meson lookup_not_eq_zero_eq_in_keys)
+      with j have "\<not>keys mon' \<subseteq> {i}"
+        by blast
+      thus ?thesis by simp
+    qed
+    hence "coeff (Var i * mpoly_of_poly i p) mon = 0"
+      unfolding eq by (intro Sum_any_zeroI) (auto simp: when_def)
+    thus ?thesis using False
+      by (simp add: mpoly_coeff_Const)
+  next
+    case True
+    define n where "n = Poly_Mapping.lookup mon i"
+    have mon_eq: "mon = Poly_Mapping.single i n"
+      using True unfolding n_def
+      by (metis Diff_eq_empty_iff add_cancel_right_left keys_empty_iff remove_key_keys remove_key_sum)
+    have eq': "mon = moni + mon' \<longleftrightarrow> n > 0 \<and> mon' = Poly_Mapping.single i (n - 1)" for mon'
+    proof safe
+      assume eq: "mon = moni + mon'"
+      thus "n > 0" "mon' = Poly_Mapping.single i (n - 1)"
+        unfolding moni_def mon_eq using gr0I by (force simp: single_diff)+
+    next
+      assume "n > 0" "mon' = Poly_Mapping.single i (n - 1)"
+      thus "mon = moni + Poly_Mapping.single i (n - 1)"
+        unfolding mon_eq moni_def by (subst single_add [symmetric]) auto
+    qed
+    have "coeff (Var i * mpoly_of_poly i p) mon = (poly.coeff p (n - 1) when (n > 0))"
+      unfolding eq eq' by (auto simp: when_def)
+    thus ?thesis
+      by (auto simp: mon_eq when_def mpoly_coeff_Const coeff_pCons split: nat.splits)
+  qed
+qed
+
+lemma mpoly_of_poly_1 [simp]: "mpoly_of_poly i 1 = 1"
+  unfolding one_pCons mpoly_of_poly_pCons mpoly_of_poly_0 by simp
+
+lemma mpoly_of_poly_uminus [simp]: "mpoly_of_poly i (-p) = -mpoly_of_poly i p"
+  by (rule mpoly_eqI) (auto simp: coeff_mpoly_of_poly when_def)
+
+lemma mpoly_of_poly_add [simp]: "mpoly_of_poly i (p + q) = mpoly_of_poly i p + mpoly_of_poly i q"
+  by (rule mpoly_eqI) (auto simp: coeff_mpoly_of_poly when_def)
+
+lemma mpoly_of_poly_diff [simp]: "mpoly_of_poly i (p - q) = mpoly_of_poly i p - mpoly_of_poly i q"
+  by (rule mpoly_eqI) (auto simp: coeff_mpoly_of_poly when_def)
+
+lemma mpoly_of_poly_smult [simp]:
+  "mpoly_of_poly i (Polynomial.smult c p) = smult c (mpoly_of_poly i p)"
+  by (rule mpoly_eqI) (auto simp: coeff_mpoly_of_poly when_def)
+
+lemma mpoly_of_poly_mult [simp]:
+  fixes p q :: "'a :: comm_semiring_1 poly"
+  shows "mpoly_of_poly i (p * q) = mpoly_of_poly i p * mpoly_of_poly i q"
+  by (induction p) (auto simp: algebra_simps smult_conv_mult_Const)
+
+lemma insertion_mpoly_of_poly [simp]: "insertion f (mpoly_of_poly i p) = poly p (f i)"
+  by (induction p) (auto simp: insertion_add insertion_mult)
+
+lemma mapping_of_mpoly_of_poly [simp]: "mapping_of (mpoly_of_poly i p) = mpoly_of_poly_aux i p"
+  by transfer' simp
+
+lemma vars_mpoly_of_poly: "vars (mpoly_of_poly i p) \<subseteq> {i}"
+proof -
+  have "x = i" if "xa \<in> keys (mpoly_of_poly_aux i p)" "x \<in> keys xa" for x xa
+    using that
+    by (meson in_mono lookup_eq_zero_in_keys_contradict mpoly_of_poly_aux.rep_eq singletonD)
+  thus ?thesis
+    by (auto simp: vars_def)
+qed
+
+lemma mpoly_map_vars_mpoly_of_poly [simp]:
+  assumes "bij f"
+  shows   "mpoly_map_vars f (mpoly_of_poly i p) = mpoly_of_poly (f i) p"
+proof (rule mpoly_eqI, goal_cases)
+  case (1 mon)
+  have "f -` keys mon \<subseteq> {i} \<longleftrightarrow> keys mon \<subseteq> {f i}"
+    using assms by (simp add: vimage_subset_eq)
+  thus ?case using assms
+    by (simp add: coeff_mpoly_map_vars coeff_mpoly_of_poly lookup_permutep keys_permutep when_def)
+qed
+
+end
\ No newline at end of file
diff --git a/thys/Hermite_Lindemann/More_Polynomial_HLW.thy b/thys/Hermite_Lindemann/More_Polynomial_HLW.thy
new file mode 100644
--- /dev/null
+++ b/thys/Hermite_Lindemann/More_Polynomial_HLW.thy
@@ -0,0 +1,518 @@
+(*
+  File:     More_Polynomial_HLW.thy
+  Author:   Manuel Eberl, TU München
+*)
+section \<open>Auxiliary facts about univariate polynomials\<close>
+theory More_Polynomial_HLW
+imports
+  "HOL-Computational_Algebra.Computational_Algebra"
+  "Polynomial_Factorization.Gauss_Lemma"
+  "Power_Sum_Polynomials.Power_Sum_Polynomials_Library"
+  "Algebraic_Numbers.Algebraic_Numbers"
+begin
+
+instance poly :: ("{idom_divide,normalization_semidom_multiplicative,factorial_ring_gcd,
+                    semiring_gcd_mult_normalize}") factorial_semiring_multiplicative ..
+
+lemma lead_coeff_prod_mset:
+  fixes A :: "'a::{comm_semiring_1, semiring_no_zero_divisors} poly multiset"
+  shows "Polynomial.lead_coeff (prod_mset A) = prod_mset (image_mset Polynomial.lead_coeff A)"
+  by (induction A) (auto simp: Polynomial.lead_coeff_mult)
+
+lemma content_normalize [simp]:
+  fixes p :: "'a :: {factorial_semiring, idom_divide, semiring_gcd, normalization_semidom_multiplicative} poly"
+  shows "content (normalize p) = content p"
+proof (cases "p = 0")
+  case [simp]: False
+  have "content p = content (unit_factor p * normalize p)"
+    by simp
+  also have "\<dots> = content (unit_factor p) * content (normalize p)"
+    by (rule content_mult)
+  also have "content (unit_factor p) = 1"
+    by (auto simp: unit_factor_poly_def)
+  finally show ?thesis by simp
+qed auto
+
+lemma rat_to_normalized_int_poly_exists:
+  fixes p :: "rat poly"
+  assumes "p \<noteq> 0"
+  obtains q lc where "p = Polynomial.smult lc (of_int_poly q)" "lc > 0" "content q = 1"
+proof -
+  define lc where "lc = fst (rat_to_normalized_int_poly p)"
+  define q where "q = snd (rat_to_normalized_int_poly p)"
+  have eq: "rat_to_normalized_int_poly p = (lc, q)"
+    by (simp add: lc_def q_def)
+  show ?thesis
+    using rat_to_normalized_int_poly[OF eq] assms
+    by (intro that[of lc q]) auto
+qed
+
+lemma irreducible_imp_squarefree:
+  assumes "irreducible p"
+  shows   "squarefree p"
+proof (rule squarefreeI)
+  fix q assume "q ^ 2 dvd p"
+  then obtain r where qr: "p = q ^ 2 * r"
+    by (elim dvdE)
+  have "q dvd 1 \<or> q * r dvd 1"
+    by (intro irreducibleD[OF assms]) (use qr in \<open>simp_all add: power2_eq_square mult_ac\<close>)
+  thus "q dvd 1"
+    by (meson dvd_mult_left)
+qed
+
+lemma squarefree_imp_rsquarefree:
+  fixes p :: "'a :: idom poly"
+  assumes "squarefree p"
+  shows   "rsquarefree p"
+  unfolding rsquarefree_def
+proof (intro conjI allI)
+  fix x :: 'a
+  have "Polynomial.order x p < 2"
+  proof (rule ccontr)
+    assume "\<not>(Polynomial.order x p < 2)"
+    hence "[:-x, 1:] ^ 2 dvd p"
+      by (subst order_divides) auto
+    from assms and this have "[:-x, 1:] dvd 1"
+      by (rule squarefreeD)
+    hence "Polynomial.degree [:-x, 1:] \<le> Polynomial.degree (1 :: 'a poly)"
+      by (rule dvd_imp_degree_le) auto
+    thus False by simp
+  qed
+  thus "Polynomial.order x p = 0 \<or> Polynomial.order x p = 1"
+    by linarith
+qed (use assms in auto)
+
+lemma squarefree_imp_coprime_pderiv:
+  fixes p :: "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize,semiring_char_0} poly"
+  assumes "squarefree p" and "content p = 1"
+  shows   "Rings.coprime p (pderiv p)"
+proof (rule coprimeI_primes)
+  fix d assume d: "prime d" "d dvd p" "d dvd pderiv p"
+  show False
+  proof (cases "Polynomial.degree d = 0")
+    case deg: False
+    obtain q where dq: "p = d * q"
+      using d by (elim dvdE)
+    have \<open>d dvd q * pderiv d\<close>
+      using d by (simp add: dq pderiv_mult dvd_add_right_iff)
+    moreover have "\<not>d dvd pderiv d"
+    proof
+      assume "d dvd pderiv d"
+      hence "Polynomial.degree d \<le> Polynomial.degree (pderiv d)"
+        using d deg by (intro dvd_imp_degree_le) (auto simp: pderiv_eq_0_iff)
+      hence "Polynomial.degree d = 0"
+        by (subst (asm) degree_pderiv) auto
+      thus False using deg by contradiction
+    qed
+    ultimately have "d dvd q"
+      using d(1) by (simp add: prime_dvd_mult_iff)
+    hence "d ^ 2 dvd p"
+      by (auto simp: dq power2_eq_square)
+    from assms(1) and this have "is_unit d"
+      by (rule squarefreeD)
+    thus False using \<open>prime d\<close> by auto
+  next
+    case True
+    then obtain d' where [simp]: "d = [:d':]"
+      by (elim degree_eq_zeroE)
+    from d have "d' dvd content p"
+      by (simp add: const_poly_dvd_iff_dvd_content)
+    with assms and prime_imp_prime_elem[OF \<open>prime d\<close>] show False
+      by (auto simp: prime_elem_const_poly_iff)
+  qed
+qed (use assms in auto)
+
+lemma irreducible_imp_coprime_pderiv:
+  fixes p :: "'a :: {idom_divide,semiring_char_0} poly"
+  assumes "irreducible p" "Polynomial.degree p \<noteq> 0"
+  shows   "Rings.coprime p (pderiv p)"
+proof (rule Rings.coprimeI)
+  fix d assume d: "d dvd p" "d dvd pderiv p"
+  obtain q where dq: "p = d * q"
+    using d by (elim dvdE)
+  have "is_unit d \<or> is_unit q"
+    using assms dq by (auto simp: irreducible_def)
+  thus "is_unit d"
+  proof
+    assume unit: "is_unit q"
+    with d have "p dvd pderiv p"
+      using algebraic_semidom_class.mult_unit_dvd_iff dq by blast
+    hence "Polynomial.degree p = 0"
+      by (meson not_dvd_pderiv)
+    with assms(2) show ?thesis by contradiction
+  qed
+qed
+
+lemma poly_gcd_eq_0I:
+  assumes "poly p x = 0" "poly q x = 0"
+  shows   "poly (gcd p q) x = 0"
+  using assms by (simp add: poly_eq_0_iff_dvd)
+
+lemma poly_eq_0_coprime:
+  assumes "Rings.coprime p q" "p \<noteq> 0" "q \<noteq> 0"
+  shows   "poly p x \<noteq> 0 \<or> poly q x \<noteq> 0"
+proof -
+  have False if "poly p x = 0" "poly q x = 0"
+  proof -
+    have "[:-x, 1:] dvd p" "[:-x, 1:] dvd q"
+      using that by (simp_all add: poly_eq_0_iff_dvd)
+    hence "[:-x, 1:] dvd 1"
+      using \<open>Rings.coprime p q\<close> by (meson not_coprimeI)
+    thus False
+      by (simp add: is_unit_poly_iff)
+  qed
+  thus ?thesis
+    by blast
+qed
+
+lemma coprime_of_int_polyI:
+  assumes "Rings.coprime p q"
+  shows   "Rings.coprime (of_int_poly p) (of_int_poly q :: 'a :: {field_char_0,field_gcd} poly)"
+  using assms gcd_of_int_poly[of p q, where ?'a = 'a] unfolding coprime_iff_gcd_eq_1 by simp
+
+lemma irreducible_imp_rsquarefree_of_int_poly:
+  fixes p :: "int poly"
+  assumes "irreducible p" and "Polynomial.degree p > 0"
+  shows   "rsquarefree (of_int_poly p :: 'a :: {field_gcd, field_char_0} poly)"
+proof -
+  {
+    fix x :: 'a
+    assume x: "poly (of_int_poly p) x = 0" "poly (pderiv (of_int_poly p)) x = 0"
+    define d where "d = gcd (of_int_poly p) (pderiv (of_int_poly p) :: 'a poly)"
+    have "poly d x = 0"
+      using x unfolding d_def by (intro poly_gcd_eq_0I) auto
+    moreover have "d \<noteq> 0"
+      using assms by (auto simp: d_def)
+    ultimately have "0 < Polynomial.degree d"
+      by (intro Nat.gr0I) (auto elim!: degree_eq_zeroE)
+    also have "Polynomial.degree d = Polynomial.degree (gcd p (pderiv p))"
+      unfolding d_def of_int_hom.map_poly_pderiv[symmetric] gcd_of_int_poly by simp
+    finally have deg: "\<dots> > 0" .
+  
+    have "gcd p (pderiv p) dvd p"
+      by auto
+    from irreducibleD'[OF assms(1) this] and deg have "p dvd gcd p (pderiv p)"
+      by auto
+    also have "\<dots> dvd pderiv p"
+      by auto
+    finally have "Polynomial.degree p = 0"
+      by auto
+    with assms have False by simp
+  }
+  thus ?thesis by (auto simp: rsquarefree_roots)
+qed
+
+lemma squarefree_of_int_polyI:
+  assumes "squarefree p" "content p = 1"
+  shows   "squarefree (of_int_poly p :: 'a :: {field_char_0,field_gcd} poly)"
+proof -
+  have "Rings.coprime p (pderiv p)"
+    by (rule squarefree_imp_coprime_pderiv) fact+
+  hence "Rings.coprime (of_int_poly p :: 'a poly) (of_int_poly (pderiv p))"
+    by (rule coprime_of_int_polyI)
+  also have "of_int_poly (pderiv p) = pderiv (of_int_poly p :: 'a poly)"
+    by (simp add: of_int_hom.map_poly_pderiv)
+  finally show ?thesis
+    using coprime_pderiv_imp_squarefree by blast
+qed
+
+lemma higher_pderiv_pcompose_linear:
+   "(pderiv ^^ n) (pcompose p [:0, c:]) =
+    Polynomial.smult (c ^ n) (pcompose ((pderiv ^^ n) p) [:0, c:])"
+  by (induction n)  (simp_all add: pderiv_pcompose pderiv_smult pderiv_pCons pcompose_smult mult_ac)
+
+lemma poly_poly_eq:
+  "poly (poly p [:x:]) y = poly (eval_poly (\<lambda>p. [:poly p y:]) p [:0, 1:]) x"
+  by (induction p) (auto simp: eval_poly_def)
+
+lemma poly_poly_poly_y_x [simp]:
+  fixes p :: "'a :: idom poly poly"
+  shows "poly (poly (poly_y_x p) [:y:]) x = poly (poly p [:x:]) y"
+proof (induction p)
+  case (pCons a p)
+  have "poly (poly (poly_y_x (pCons a p)) [:y:]) x = 
+          poly a y + poly (poly (map_poly (pCons 0) (poly_y_x p)) [:y:]) x"
+    by (simp add: poly_y_x_pCons eval_poly_def)
+  also have "pCons 0 = (\<lambda>p::'a poly. Polynomial.monom 1 1 * p)"
+    by (simp add: Polynomial.monom_altdef)
+  also have "map_poly \<dots> (poly_y_x p) = Polynomial.smult (Polynomial.monom 1 1) (poly_y_x p)"
+    by (simp add: smult_conv_map_poly)
+  also have "poly \<dots> [:y:] = Polynomial.monom 1 1 * poly (poly_y_x p) [:y:]"
+    by simp
+  also have "poly a y + poly \<dots> x = poly (poly (pCons a p) [:x:]) y"
+    by (simp add: pCons poly_monom)
+  finally show ?case .
+qed auto
+
+lemma (in idom_hom) map_poly_higher_pderiv [hom_distribs]:
+  "map_poly hom ((pderiv ^^ n) p) = (pderiv ^^ n) (map_poly hom p)"
+  by (induction n) (simp_all add: map_poly_pderiv)
+
+lemma coeff_prod_linear_factors:
+  fixes f :: "'a \<Rightarrow> 'b :: comm_ring_1"
+  assumes [intro]: "finite A"
+  shows "Polynomial.coeff (\<Prod>x\<in>A. [:-f x, 1:] ^ e x) i =
+           (\<Sum>X | X \<in> Pow (SIGMA x:A. {..<e x}) \<and> i = sum e A - card X.
+             (-1) ^ card X * (\<Prod>x\<in>X. f (fst x)))"
+proof -
+  define poly_X where "poly_X = (Polynomial.monom 1 1 :: 'b poly)"
+  have [simp]: "(- 1) ^ n = [:(- 1) ^ n :: 'b:]" for n :: nat
+    by (simp flip: pCons_one add: poly_const_pow)
+  have "(\<Prod>x\<in>A. [:-f x, 1:] ^ e x) = (\<Prod>(x,_)\<in>Sigma A (\<lambda>x. {..<e x}). [:-f x, 1:])"
+    by (subst prod.Sigma [symmetric]) auto
+  also have "\<dots> = (\<Prod>(x,_)\<in>Sigma A (\<lambda>x. {..<e x}). poly_X - [:f x:])"
+    by (intro prod.cong) (auto simp: poly_X_def monom_altdef)
+  also have "\<dots> = (\<Sum>X\<in>Pow (SIGMA x:A. {..<e x}).
+                    Polynomial.smult ((-1) ^ card X * (\<Prod>x\<in>X. f (fst x)))
+                    (poly_X ^ card ((SIGMA x:A. {..<e x}) - X)))"
+    unfolding case_prod_unfold 
+    by (subst prod_diff1) (auto simp: mult_ac simp flip: coeff_lift_hom.hom_prod)
+  also have "\<dots> = (\<Sum>X\<in>Pow (SIGMA x:A. {..<e x}).
+       Polynomial.monom ((- 1) ^ card X * (\<Prod>x\<in>X. f (fst x))) (card ((SIGMA x:A. {..<e x}) - X)))"
+    unfolding poly_X_def monom_power Polynomial.smult_monom by simp
+  also have "Polynomial.coeff \<dots> i = (\<Sum>X\<in>{X\<in>Pow (SIGMA x:A. {..<e x}). i =
+               sum e A - card X}. (- 1) ^ card X * (\<Prod>x\<in>X. f (fst x)))"
+    unfolding Polynomial.coeff_sum
+  proof (intro sum.mono_neutral_cong_right ballI, goal_cases)
+    case (3 X)
+    hence X: "X \<subseteq> (SIGMA x:A. {..<e x})"
+      by auto
+    have card_le: "card X \<le> card (SIGMA x:A. {..<e x})"
+      using X by (intro card_mono) auto
+    have "finite X"
+      by (rule finite_subset[OF X]) auto
+    hence "card ((SIGMA x:A. {..<e x}) - X) = card (SIGMA x:A. {..<e x}) - card X"
+      using 3 by (intro card_Diff_subset) auto
+    also have card_eq: "card (SIGMA x:A. {..<e x}) = sum e A"
+      by (subst card_SigmaI) auto
+    finally show ?case
+      using 3 card_le card_eq by (auto simp: algebra_simps)
+  next
+    case (4 X)
+    hence X: "X \<subseteq> (SIGMA x:A. {..<e x})"
+      by auto
+    have "finite X"
+      by (rule finite_subset[OF X]) auto
+    hence "card ((SIGMA x:A. {..<e x}) - X) = card (SIGMA x:A. {..<e x}) - card X"
+      using 4 by (intro card_Diff_subset) auto
+    also have card_eq: "card (SIGMA x:A. {..<e x}) = sum e A"
+      by (subst card_SigmaI) auto
+    finally show ?case
+      using 4 card_eq by (auto simp: algebra_simps)
+  qed auto
+  finally show ?thesis .
+qed
+
+lemma (in comm_ring_hom) synthetic_div_hom:
+  "synthetic_div (map_poly hom p) (hom x) = map_poly hom (synthetic_div p x)"
+  by (induction p) (auto simp: map_poly_pCons_hom)
+
+lemma synthetic_div_altdef:
+  fixes p :: "'a :: field poly"
+  shows "synthetic_div p c = p div [:-c, 1:]"
+proof -
+  define q where "q = p div [:- c, 1:]"
+  have "Polynomial.degree (p mod [:-c, 1:]) = 0"
+  proof (cases "p mod [:-c, 1:] = 0")
+    case False
+    hence "Polynomial.degree (p mod [:-c, 1:]) < Polynomial.degree [:-c, 1:]"
+      by (intro degree_mod_less') auto
+    thus ?thesis by simp
+  qed auto
+  then obtain d where d: "p mod [:-c, 1:] = [:d:]"
+    by (elim degree_eq_zeroE)
+
+  have p_eq: "p = q * [:-c, 1:] + [:d:]"
+    unfolding q_def d [symmetric] by presburger
+  have [simp]: "poly p c = d"
+    by (simp add: p_eq)
+  have "p + Polynomial.smult c q = pCons (poly p c) q"
+    by (subst p_eq) auto
+  from synthetic_div_unique[OF this] show ?thesis
+    by (auto simp: q_def)
+qed
+
+lemma (in ring_closed) poly_closed [intro]:
+  assumes "\<And>i. poly.coeff p i \<in> A" "x \<in> A"
+  shows   "poly p x \<in> A"
+  unfolding poly_altdef by (intro sum_closed mult_closed power_closed assms)
+
+lemma (in ring_closed) coeff_pCons_closed [intro]:
+  assumes "\<And>i. poly.coeff p i \<in> A" "x \<in> A"
+  shows   "poly.coeff (pCons x p) i \<in> A"
+  unfolding poly_altdef using assms by (auto simp: coeff_pCons split: nat.splits)
+
+lemma (in ring_closed) coeff_poly_mult_closed [intro]:
+  assumes "\<And>i. poly.coeff p i \<in> A" "\<And>i. poly.coeff q i \<in> A"
+  shows   "poly.coeff (p * q) i \<in> A"
+  unfolding coeff_mult using assms by auto
+
+lemma (in ring_closed) coeff_poly_prod_closed [intro]:
+  assumes "\<And>x i. x \<in> X \<Longrightarrow> poly.coeff (f x) i \<in> A"
+  shows   "poly.coeff (prod f X) i \<in> A"
+  using assms by (induction X arbitrary: i rule: infinite_finite_induct) auto
+
+lemma (in ring_closed) coeff_poly_power_closed [intro]:
+  assumes "\<And>i. poly.coeff p i \<in> A"
+  shows   "poly.coeff (p ^ n) i \<in> A"
+  using coeff_poly_prod_closed[of "{..<n}" "\<lambda>_. p" i] assms by simp
+
+lemma (in ring_closed) synthetic_div_closed:
+  assumes "\<And>i. poly.coeff p i \<in> A" "x \<in> A"
+  shows   "poly.coeff (synthetic_div p x) i \<in> A"
+proof -
+  from assms(1) have "\<forall>i. poly.coeff p i \<in> A"
+    by blast
+  from this and assms(2) show ?thesis
+    by (induction p arbitrary: i) (auto simp: coeff_pCons split: nat.splits)
+qed
+
+lemma pcompose_monom: "pcompose (Polynomial.monom c n) p = Polynomial.smult c (p ^ n)"
+  by (simp add: monom_altdef pcompose_hom.hom_power pcompose_smult)
+
+lemma poly_roots_uminus [simp]: "poly_roots (-p) = poly_roots p"
+  using poly_roots_smult[of "-1" p] by (simp del: poly_roots_smult)
+
+lemma poly_roots_normalize [simp]:
+  fixes p :: "'a :: {normalization_semidom, idom_divide} poly"
+  shows "poly_roots (normalize p) = poly_roots p"
+proof (cases "p = 0")
+  case [simp]: False
+  have "poly_roots p = poly_roots (unit_factor p * normalize p)"
+    by simp
+  also have "\<dots> = poly_roots (normalize p)"
+    unfolding unit_factor_poly_def by simp
+  finally show ?thesis ..
+qed auto
+
+
+lemma poly_roots_of_int_normalize [simp]:
+  "poly_roots (of_int_poly (normalize p) :: 'a :: {idom, ring_char_0} poly) =
+   poly_roots (of_int_poly p)"
+proof (cases "p = 0")
+  case [simp]: False
+  have "poly_roots (of_int_poly p :: 'a poly) = poly_roots (of_int_poly (unit_factor p * normalize p))"
+    by simp
+  also have "\<dots> = poly_roots (Polynomial.smult (of_int (sgn (Polynomial.lead_coeff p)))
+                    (of_int_poly (normalize p)))"
+    by (simp add: unit_factor_poly_def of_int_hom.map_poly_hom_smult)
+  also have "\<dots> = poly_roots (Ring_Hom_Poly.of_int_poly (normalize p) :: 'a poly)"
+    by (intro poly_roots_smult) (auto simp: sgn_if)
+  finally show ?thesis ..
+qed auto
+
+lemma poly_roots_power [simp]: "poly_roots (p ^ n) = repeat_mset n (poly_roots p)"
+proof (cases "p = 0")
+  case True
+  thus ?thesis by (cases n) auto
+next
+  case False
+  thus ?thesis by (induction n) (auto simp: poly_roots_mult)
+qed
+
+lemma poly_roots_conv_sum_prime_factors:
+  "poly_roots q = (\<Sum>p\<in>#prime_factorization q. poly_roots p)"
+proof (cases "q = 0")
+  case [simp]: False
+
+  have "(\<Sum>p\<in>#prime_factorization q. poly_roots p) =
+        poly_roots (prod_mset (prime_factorization q))"
+    by (rule poly_roots_prod_mset [symmetric]) auto
+  also have "\<dots> = poly_roots (normalize (prod_mset (prime_factorization q)))"
+    by simp
+  also have "normalize (prod_mset (prime_factorization q)) = normalize q"
+    by (rule prod_mset_prime_factorization_weak) auto
+  also have "poly_roots \<dots> = poly_roots q"
+    by simp
+  finally show ?thesis ..
+qed auto
+
+lemma poly_roots_of_int_conv_sum_prime_factors:
+  "poly_roots (of_int_poly q :: 'a :: {idom, ring_char_0} poly) =
+   (\<Sum>p\<in>#prime_factorization q. poly_roots (of_int_poly p))"
+proof (cases "q = 0")
+  case [simp]: False
+
+  have "(\<Sum>p\<in>#prime_factorization q. poly_roots (of_int_poly p :: 'a poly)) =
+        poly_roots (\<Prod>p\<in>#prime_factorization q. of_int_poly p)"
+    by (subst poly_roots_prod_mset) (auto simp: multiset.map_comp o_def)
+  also have "(\<Prod>p\<in>#prime_factorization q. of_int_poly p :: 'a poly) =
+               of_int_poly (prod_mset (prime_factorization q))"
+    by simp
+  also have "poly_roots \<dots> = poly_roots (of_int_poly (normalize (prod_mset (prime_factorization q))))"
+    by (rule poly_roots_of_int_normalize [symmetric])
+  also have "normalize (prod_mset (prime_factorization q)) = normalize q"
+    by (rule prod_mset_prime_factorization_weak) auto
+  also have "poly_roots (of_int_poly \<dots> :: 'a poly) = poly_roots (of_int_poly q)"
+    by simp
+  finally show ?thesis ..
+qed auto
+
+lemma dvd_imp_poly_roots_subset:
+  assumes "q \<noteq> 0" "p dvd q"
+  shows   "poly_roots p \<subseteq># poly_roots q"
+proof -
+  from assms have "p \<noteq> 0"
+    by auto
+  thus ?thesis
+    using assms by (intro mset_subset_eqI) (auto intro: dvd_imp_order_le)
+qed
+
+lemma abs_prod_mset: "\<bar>prod_mset (A :: 'a :: idom_abs_sgn multiset)\<bar> = prod_mset (image_mset abs A)"
+  by (induction A) (auto simp: abs_mult)
+
+lemma content_1_imp_nonconstant_prime_factors:
+  assumes "content (p :: int poly) = 1" and "q \<in> prime_factors p"
+  shows   "Polynomial.degree q > 0"
+proof -
+  let ?d = "Polynomial.degree :: int poly \<Rightarrow> nat"
+  let ?lc = "Polynomial.lead_coeff :: int poly \<Rightarrow> int"
+  define P where "P = prime_factorization p"
+  define P1 where "P1 = filter_mset (\<lambda>p. ?d p = 0) P"
+  define P2 where "P2 = filter_mset (\<lambda>p. ?d p > 0) P"
+  have [simp]: "p \<noteq> 0"
+    using assms by auto
+  have "1 = content (normalize p)"
+    using assms by simp
+  also have "normalize p = prod_mset P"
+    unfolding P_def by (rule prod_mset_prime_factorization [symmetric]) auto
+  also have "P = filter_mset (\<lambda>p. ?d p = 0) P + filter_mset (\<lambda>p. ?d p > 0) P"
+    by (induction P) auto
+  also have "prod_mset \<dots> = prod_mset P1 * prod_mset P2"
+    unfolding P1_def P2_def by (subst prod_mset.union) auto
+  also have "content \<dots> = content (prod_mset P1) * content (prod_mset P2)"
+    unfolding content_mult ..
+  also have "image_mset id P1 = image_mset (\<lambda>q. [:?lc q:]) P1"
+    by (intro image_mset_cong) (auto simp: P1_def elim!: degree_eq_zeroE)
+  hence "P1 = image_mset (\<lambda>q. [:?lc q:]) P1"
+    by simp
+  also have "content (prod_mset \<dots>) = \<bar>(\<Prod>q\<in>#P1. ?lc q)\<bar>"
+    by (simp add: content_prod_mset multiset.map_comp o_def abs_prod_mset)
+  finally have "\<bar>(\<Prod>q\<in>#P1. ?lc q)\<bar> * content (prod_mset P2) = 1" ..
+  hence "\<bar>(\<Prod>q\<in>#P1. ?lc q)\<bar> dvd 1"
+    unfolding dvd_def by metis
+
+  have "set_mset P1 = {}"
+  proof (rule ccontr)
+    assume "set_mset P1 \<noteq> {}"
+    then obtain q where q: "q \<in># P1"
+      by blast
+    have "\<bar>?lc q\<bar> dvd (\<Prod>q\<in>#P1. \<bar>?lc q\<bar>)"
+      by (rule dvd_prod_mset) (use q in auto)
+    also have "\<dots> = \<bar>(\<Prod>q\<in>#P1. ?lc q)\<bar>"
+      by (simp add: abs_prod_mset multiset.map_comp o_def)
+    also have "\<dots> dvd 1"
+      by fact
+    finally have "is_unit (?lc q)"
+      by simp
+    hence "is_unit q"
+      using q unfolding P1_def by (auto elim!: degree_eq_zeroE)
+    moreover have "prime q"
+      using q unfolding P1_def P_def by auto
+    ultimately show False by auto
+  qed
+  with assms show ?thesis
+    by (auto simp: P1_def P_def)
+qed
+
+end
\ No newline at end of file
diff --git a/thys/Hermite_Lindemann/ROOT b/thys/Hermite_Lindemann/ROOT
new file mode 100644
--- /dev/null
+++ b/thys/Hermite_Lindemann/ROOT
@@ -0,0 +1,14 @@
+chapter AFP
+
+session Hermite_Lindemann (AFP) = "Pi_Transcendental" +
+  options [timeout = 1200]
+  sessions
+    "HOL-Library"
+    Algebraic_Numbers
+    Power_Sum_Polynomials
+  theories
+    Hermite_Lindemann
+  document_files
+    "root.tex"
+    "root.bib"
+
diff --git a/thys/Hermite_Lindemann/document/root.bib b/thys/Hermite_Lindemann/document/root.bib
new file mode 100644
--- /dev/null
+++ b/thys/Hermite_Lindemann/document/root.bib
@@ -0,0 +1,36 @@
+@book{baker,
+  series={Cambridge Mathematical Library},
+  title={Transcendental Number Theory},
+  DOI={10.1017/CBO9780511565977},
+  isbn={9780521397919},
+  publisher={Cambridge University Press},
+  author={Baker, Alan},
+  year={1975},
+}
+
+@article{redheffer_steinberg,
+author = {Robert Steinberg and Raymond Moos Redheffer},
+title = {Analytic proof of the {L}indemann theorem},
+volume = {2},
+journal = {Pacific Journal of Mathematics},
+number = {2},
+pages = {231--242},
+year = {1952},
+doi = {10.2140/pjm.1952.2.231}
+}
+
+
+@inproceedings{bernard,
+  author    = {Sophie Bernard},
+  editor    = {Mauricio Ayala{-}Rinc{\'{o}}n and
+               C{\'{e}}sar A. Mu{\~{n}}oz},
+  title     = {Formalization of the {L}indemann-{W}eierstrass Theorem},
+  booktitle = {Interactive Theorem Proving - 8th International Conference, {ITP}
+               2017, Bras{\'i}lia, Brazil, September 26-29, 2017, Proceedings},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {10499},
+  pages     = {65--80},
+  publisher = {Springer},
+  year      = {2017},
+  doi       = {10.1007/978-3-319-66107-0_5}
+}
\ No newline at end of file
diff --git a/thys/Hermite_Lindemann/document/root.tex b/thys/Hermite_Lindemann/document/root.tex
new file mode 100644
--- /dev/null
+++ b/thys/Hermite_Lindemann/document/root.tex
@@ -0,0 +1,63 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage{isabelle,isabellesym}
+\usepackage{amsfonts, amsmath, amssymb}
+
+% this should be the last package used
+\usepackage{pdfsetup}
+\usepackage[shortcuts]{extdash}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+\begin{document}
+
+\title{The Hermite--Lindemann--Weierstraß Transcendence Theorem}
+\author{Manuel Eberl}
+\maketitle
+
+\begin{abstract}
+This article provides a formalisation of the Her\-mite\--Lin\-de\-mann\--Wei\-er\-straß Theorem
+(also known as simply Her\-mite\--Lin\-de\-mann or Lin\-de\-mann\--Wei\-er\-straß).
+ This theorem is one of the crowning achievements of 19th century number theory.
+
+The theorem states that if $\alpha_1, \ldots, \alpha_n\in\mathbb{C}$ are algebraic numbers that
+are linearly independent over $\mathbb{Z}$, then $e^{\alpha_1},\ldots,e^{\alpha_n}$ are
+algebraically independent over $\mathbb{Q}$.
+
+Like the previous formalisation in Coq by Bernard~\cite{bernard}, I proceeded by formalising 
+Baker's alternative formulation of the theorem~\cite{baker} and then deriving the original one from
+that. Baker's version states that for any algebraic numbers
+$\beta_1, \ldots, \beta_n\in\mathbb{C}$ and distinct algebraic numbers
+$\alpha_i, \ldots, \alpha_n\in\mathbb{C}$, we have:
+\[\beta_1 e^{\alpha_1} + \ldots + \beta_n e^{\alpha_n} = 0 \quad\quad\text{iff}\quad\quad
+  \forall i.\ \beta_i = 0\]
+
+This has a number of immediate corollaries, e.g.:
+\begin{itemize}
+\item $e$ and $\pi$ are transcendental
+\item $e^z$, $\sin z$, $\tan z$, etc.\ are transcendental for algebraic $z\in\mathbb{C}\setminus\{0\}$
+\item $\ln z$ is transcendental for algebraic $z\in\mathbb{C}\setminus\{0, 1\}$
+\end{itemize}
+\end{abstract}
+
+\newpage
+\tableofcontents
+\newpage
+\parindent 0pt\parskip 0.5ex
+
+\input{session}
+
+\nocite{baker}
+\nocite{redheffer_steinberg}
+\nocite{bernard}
+
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff --git a/thys/ROOTS b/thys/ROOTS
--- a/thys/ROOTS
+++ b/thys/ROOTS
@@ -1,589 +1,590 @@
 ADS_Functor
 AI_Planning_Languages_Semantics
 AODV
 AVL-Trees
 AWN
 Abortable_Linearizable_Modules
 Abs_Int_ITP2012
 Abstract-Hoare-Logics
 Abstract-Rewriting
 Abstract_Completeness
 Abstract_Soundness
 Adaptive_State_Counting
 Affine_Arithmetic
 Aggregation_Algebras
 Akra_Bazzi
 Algebraic_Numbers
 Algebraic_VCs
 Allen_Calculus
 Amicable_Numbers
 Amortized_Complexity
 AnselmGod
 Applicative_Lifting
 Approximation_Algorithms
 Architectural_Design_Patterns
 Aristotles_Assertoric_Syllogistic
 Arith_Prog_Rel_Primes
 ArrowImpossibilityGS
 Attack_Trees
 Auto2_HOL
 Auto2_Imperative_HOL
 AutoFocus-Stream
 Automated_Stateful_Protocol_Verification
 Automatic_Refinement
 AxiomaticCategoryTheory
 BDD
 BNF_CC
 BNF_Operations
 BTree
 Banach_Steinhaus
 Bell_Numbers_Spivey
 Berlekamp_Zassenhaus
 Bernoulli
 Bertrands_Postulate
 Bicategory
 BinarySearchTree
 Binding_Syntax_Theory
 Binomial-Heaps
 Binomial-Queues
 BirdKMP
 Blue_Eyes
 Bondy
 Boolean_Expression_Checkers
 Bounded_Deducibility_Security
 Buchi_Complementation
 Budan_Fourier
 Buffons_Needle
 Buildings
 BytecodeLogicJmlTypes
 C2KA_DistributedSystems
 CAVA_Automata
 CAVA_LTL_Modelchecker
 CCS
 CISC-Kernel
 CRDT
 CYK
 CakeML
 CakeML_Codegen
 Call_Arity
 Card_Equiv_Relations
 Card_Multisets
 Card_Number_Partitions
 Card_Partitions
 Cartan_FP
 Case_Labeling
 Catalan_Numbers
 Category
 Category2
 Category3
 Cauchy
 Cayley_Hamilton
 Certification_Monads
 Chandy_Lamport
 Chord_Segments
 Circus
 Clean
 ClockSynchInst
 Closest_Pair_Points
 CofGroups
 Coinductive
 Coinductive_Languages
 Collections
 Comparison_Sort_Lower_Bound
 Compiling-Exceptions-Correctly
 Complete_Non_Orders
 Completeness
 Complex_Geometry
 Complx
 ComponentDependencies
 ConcurrentGC
 ConcurrentIMP
 Concurrent_Ref_Alg
 Concurrent_Revisions
 Consensus_Refined
 Constructive_Cryptography
 Constructor_Funs
 Containers
 CoreC++
 Core_DOM
 Core_SC_DOM
 Count_Complex_Roots
 CryptHOL
 CryptoBasedCompositionalProperties
 CSP_RefTK
 DFS_Framework
 DPT-SAT-Solver
 DataRefinementIBP
 Datatype_Order_Generator
 Decl_Sem_Fun_PL
 Decreasing-Diagrams
 Decreasing-Diagrams-II
 Deep_Learning
 Delta_System_Lemma
 Density_Compiler
 Dependent_SIFUM_Refinement
 Dependent_SIFUM_Type_Systems
 Depth-First-Search
 Derangements
 Deriving
 Descartes_Sign_Rule
 Dict_Construction
 Differential_Dynamic_Logic
 Differential_Game_Logic
 Dijkstra_Shortest_Path
 Diophantine_Eqns_Lin_Hom
 Dirichlet_L
 Dirichlet_Series
 DiscretePricing
 Discrete_Summation
 DiskPaxos
 DOM_Components
 DynamicArchitectures
 Dynamic_Tables
 E_Transcendental
 Echelon_Form
 EdmondsKarp_Maxflow
 Efficient-Mergesort
 Elliptic_Curves_Group_Law
 Encodability_Process_Calculi
 Epistemic_Logic
 Ergodic_Theory
 Error_Function
 Euler_MacLaurin
 Euler_Partition
 Example-Submission
 Extended_Finite_State_Machine_Inference
 Extended_Finite_State_Machines
 FFT
 FLP
 FOL-Fitting
 FOL_Harrison
 FOL_Seq_Calc1
 Factored_Transition_System_Bounding
 Falling_Factorial_Sum
 Farkas
 FeatherweightJava
 Featherweight_OCL
 Fermat3_4
 FileRefinement
 FinFun
 Finger-Trees
 Finite-Map-Extras
 Finite_Automata_HF
 First_Order_Terms
 First_Welfare_Theorem
 Fishburn_Impossibility
 Fisher_Yates
 Flow_Networks
 Floyd_Warshall
 Flyspeck-Tame
 FocusStreamsCaseStudies
 Forcing
 Formal_Puiseux_Series
 Formal_SSA
 Formula_Derivatives
 Fourier
 Free-Boolean-Algebra
 Free-Groups
 FunWithFunctions
 FunWithTilings
 Functional-Automata
 Functional_Ordered_Resolution_Prover
 Furstenberg_Topology
 GPU_Kernel_PL
 Gabow_SCC
 Game_Based_Crypto
 Gauss-Jordan-Elim-Fun
 Gauss_Jordan
 Gauss_Sums
 Gaussian_Integers
 GenClock
 General-Triangle
 Generalized_Counting_Sort
 Generic_Deriving
 Generic_Join
 GewirthPGCProof
 Girth_Chromatic
 GoedelGod
 Goedel_HFSet_Semantic
 Goedel_HFSet_Semanticless
 Goedel_Incompleteness
 Goodstein_Lambda
 GraphMarkingIBP
 Graph_Saturation
 Graph_Theory
 Green
 Groebner_Bases
 Groebner_Macaulay
 Gromov_Hyperbolicity
 Group-Ring-Module
 HOL-CSP
 HOLCF-Prelude
 HRB-Slicing
 Heard_Of
 Hello_World
 HereditarilyFinite
 Hermite
+Hermite_Lindemann
 Hidden_Markov_Models
 Higher_Order_Terms
 Hoare_Time
 Hood_Melville_Queue
 HotelKeyCards
 Huffman
 Hybrid_Logic
 Hybrid_Multi_Lane_Spatial_Logic
 Hybrid_Systems_VCs
 HyperCTL
 IEEE_Floating_Point
 IMAP-CRDT
 IMO2019
 IMP2
 IMP2_Binary_Heap
 IP_Addresses
 Imperative_Insertion_Sort
 Impossible_Geometry
 Incompleteness
 Incredible_Proof_Machine
 Inductive_Confidentiality
 Inductive_Inference
 InfPathElimination
 InformationFlowSlicing
 InformationFlowSlicing_Inter
 Integration
 Interpreter_Optimizations
 Interval_Arithmetic_Word32
 Iptables_Semantics
 Irrational_Series_Erdos_Straus
 Irrationality_J_Hancl
 Isabelle_C
 Isabelle_Marries_Dirac
 Isabelle_Meta_Model
 IsaGeoCoq
 Jacobson_Basic_Algebra
 Jinja
 JinjaDCI
 JinjaThreads
 JiveDataStoreModel
 Jordan_Hoelder
 Jordan_Normal_Form
 KAD
 KAT_and_DRA
 KBPs
 KD_Tree
 Key_Agreement_Strong_Adversaries
 Kleene_Algebra
 Knuth_Bendix_Order
 Knot_Theory
 Knuth_Bendix_Order
 Knuth_Morris_Pratt
 Koenigsberg_Friendship
 Kruskal
 Kuratowski_Closure_Complement
 LLL_Basis_Reduction
 LLL_Factorization
 LOFT
 LTL
 LTL_Master_Theorem
 LTL_Normal_Form
 LTL_to_DRA
 LTL_to_GBA
 Lam-ml-Normalization
 LambdaAuth
 LambdaMu
 Lambda_Free_EPO
 Lambda_Free_KBOs
 Lambda_Free_RPOs
 Lambert_W
 Landau_Symbols
 Laplace_Transform
 Latin_Square
 LatticeProperties
 Launchbury
 Laws_of_Large_Numbers
 Lazy-Lists-II
 Lazy_Case
 Lehmer
 Lifting_Definition_Option
 LightweightJava
 LinearQuantifierElim
 Linear_Inequalities
 Linear_Programming
 Linear_Recurrences
 Liouville_Numbers
 List-Index
 List-Infinite
 List_Interleaving
 List_Inversions
 List_Update
 LocalLexing
 Localization_Ring
 Locally-Nameless-Sigma
 Lowe_Ontological_Argument
 Lower_Semicontinuous
 Lp
 Lucas_Theorem
 MFMC_Countable
 MFODL_Monitor_Optimized
 MFOTL_Monitor
 MSO_Regex_Equivalence
 Markov_Models
 Marriage
 Mason_Stothers
 Matrices_for_ODEs
 Matrix
 Matrix_Tensor
 Matroids
 Max-Card-Matching
 Median_Of_Medians_Selection
 Menger
 Mereology
 Mersenne_Primes
 MiniML
 Minimal_SSA
 Minkowskis_Theorem
 Minsky_Machines
 Modal_Logics_for_NTS
 Modular_Assembly_Kit_Security
 Monad_Memo_DP
 Monad_Normalisation
 MonoBoolTranAlgebra
 MonoidalCategory
 Monomorphic_Monad
 MuchAdoAboutTwo
 Multi_Party_Computation
 Multirelations
 Myhill-Nerode
 Name_Carrying_Type_Inference
 Nash_Williams
 Nat-Interval-Logic
 Native_Word
 Nested_Multisets_Ordinals
 Network_Security_Policy_Verification
 Neumann_Morgenstern_Utility
 No_FTL_observers
 Nominal2
 Noninterference_CSP
 Noninterference_Concurrent_Composition
 Noninterference_Generic_Unwinding
 Noninterference_Inductive_Unwinding
 Noninterference_Ipurge_Unwinding
 Noninterference_Sequential_Composition
 NormByEval
 Nullstellensatz
 Octonions
 OpSets
 Open_Induction
 Optics
 Optimal_BST
 Orbit_Stabiliser
 Order_Lattice_Props
 Ordered_Resolution_Prover
 Ordinal
 Ordinal_Partitions
 Ordinals_and_Cardinals
 Ordinary_Differential_Equations
 PAC_Checker
 PCF
 PLM
 POPLmark-deBruijn
 PSemigroupsConvolution
 Pairing_Heap
 Paraconsistency
 Parity_Game
 Partial_Function_MR
 Partial_Order_Reduction
 Password_Authentication_Protocol
 Pell
 Perfect-Number-Thm
 Perron_Frobenius
 Physical_Quantities
 Pi_Calculus
 Pi_Transcendental
 Planarity_Certificates
 Poincare_Bendixson
 Poincare_Disc
 Polynomial_Factorization
 Polynomial_Interpolation
 Polynomials
 Pop_Refinement
 Posix-Lexing
 Possibilistic_Noninterference
 Power_Sum_Polynomials
 Pratt_Certificate
 Presburger-Automata
 Prim_Dijkstra_Simple
 Prime_Distribution_Elementary
 Prime_Harmonic_Series
 Prime_Number_Theorem
 Priority_Queue_Braun
 Priority_Search_Trees
 Probabilistic_Noninterference
 Probabilistic_Prime_Tests
 Probabilistic_System_Zoo
 Probabilistic_Timed_Automata
 Probabilistic_While
 Program-Conflict-Analysis
 Projective_Geometry
 Projective_Measurements
 Promela
 Proof_Strategy_Language
 PropResPI
 Propositional_Proof_Systems
 Prpu_Maxflow
 PseudoHoops
 Psi_Calculi
 Ptolemys_Theorem
 QHLProver
 QR_Decomposition
 Quantales
 Quaternions
 Quick_Sort_Cost
 RIPEMD-160-SPARK
 ROBDD
 RSAPSS
 Ramsey-Infinite
 Random_BSTs
 Random_Graph_Subgraph_Threshold
 Randomised_BSTs
 Randomised_Social_Choice
 Rank_Nullity_Theorem
 Real_Impl
 Recursion-Addition
 Recursion-Theory-I
 Refine_Imperative_HOL
 Refine_Monadic
 RefinementReactive
 Regex_Equivalence
 Regular-Sets
 Regular_Algebras
 Relation_Algebra
 Relational-Incorrectness-Logic
 Relational_Disjoint_Set_Forests
 Relational_Method
 Relational_Minimum_Spanning_Trees
 Relational_Paths
 Rep_Fin_Groups
 Residuated_Lattices
 Resolution_FOL
 Rewriting_Z
 Ribbon_Proofs
 Robbins-Conjecture
 Robinson_Arithmetic
 Root_Balanced_Tree
 Routing
 Roy_Floyd_Warshall
 SATSolverVerification
 SC_DOM_Components
 SDS_Impossibility
 SIFPL
 SIFUM_Type_Systems
 SPARCv8
 Safe_Distance
 Safe_OCL
 Saturation_Framework
 Saturation_Framework_Extensions
 Shadow_DOM
 Secondary_Sylow
 Security_Protocol_Refinement
 Selection_Heap_Sort
 SenSocialChoice
 Separata
 Separation_Algebra
 Separation_Logic_Imperative_HOL
 SequentInvertibility
 Shadow_SC_DOM
 Shivers-CFA
 ShortestPath
 Show
 Sigma_Commit_Crypto
 Signature_Groebner
 Simpl
 Simple_Firewall
 Simplex
 Skew_Heap
 Skip_Lists
 Slicing
 Sliding_Window_Algorithm
 Smith_Normal_Form
 Smooth_Manifolds
 Sort_Encodings
 Source_Coding_Theorem
 Special_Function_Bounds
 Splay_Tree
 Sqrt_Babylonian
 Stable_Matching
 Statecharts
 Stateful_Protocol_Composition_and_Typing
 Stellar_Quorums
 Stern_Brocot
 Stewart_Apollonius
 Stirling_Formula
 Stochastic_Matrices
 Stone_Algebras
 Stone_Kleene_Relation_Algebras
 Stone_Relation_Algebras
 Store_Buffer_Reduction
 Stream-Fusion
 Stream_Fusion_Code
 Strong_Security
 Sturm_Sequences
 Sturm_Tarski
 Stuttering_Equivalence
 Subresultants
 Subset_Boolean_Algebras
 SumSquares
 Sunflowers
 SuperCalc
 Surprise_Paradox
 Symmetric_Polynomials
 Syntax_Independent_Logic
 Szpilrajn
 TESL_Language
 TLA
 Tail_Recursive_Functions
 Tarskis_Geometry
 Taylor_Models
 Timed_Automata
 Topological_Semantics
 Topology
 TortoiseHare
 Transcendence_Series_Hancl_Rucki
 Transformer_Semantics
 Transition_Systems_and_Automata
 Transitive-Closure
 Transitive-Closure-II
 Treaps
 Tree-Automata
 Tree_Decomposition
 Triangle
 Trie
 Twelvefold_Way
 Tycon
 Types_Tableaus_and_Goedels_God
 UPF
 UPF_Firewall
 UTP
 Universal_Turing_Machine
 UpDown_Scheme
 Valuation
 VectorSpace
 VeriComp
 Verified-Prover
 Verified_SAT_Based_AI_Planning
 VerifyThis2018
 VerifyThis2019
 Vickrey_Clarke_Groves
 VolpanoSmith
 WHATandWHERE_Security
 WOOT_Strong_Eventual_Consistency
 WebAssembly
 Weight_Balanced_Trees
 Well_Quasi_Orders
 Winding_Number_Eval
 Word_Lib
 WorkerWrapper
 XML
 ZFC_in_HOL
 Zeta_3_Irrational
 Zeta_Function
 pGCL