author Manuel Eberl Mon, 04 Feb 2019 12:16:03 +0100 changeset 69785 9e326f6f8a24 parent 69784 24bbc4e30e5b child 69786 a5732629cc46
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
 CONTRIBUTORS file | annotate | diff | comparison | revisions NEWS file | annotate | diff | comparison | revisions src/HOL/Algebra/Multiplicative_Group.thy file | annotate | diff | comparison | revisions src/HOL/Computational_Algebra/Factorial_Ring.thy file | annotate | diff | comparison | revisions src/HOL/Divides.thy file | annotate | diff | comparison | revisions src/HOL/GCD.thy file | annotate | diff | comparison | revisions src/HOL/Number_Theory/Number_Theory.thy file | annotate | diff | comparison | revisions src/HOL/Number_Theory/Pocklington.thy file | annotate | diff | comparison | revisions src/HOL/Number_Theory/Residue_Primitive_Roots.thy file | annotate | diff | comparison | revisions src/HOL/Number_Theory/Residues.thy file | annotate | diff | comparison | revisions src/HOL/Number_Theory/Totient.thy file | annotate | diff | comparison | revisions src/HOL/Number_Theory/document/root.bib file | annotate | diff | comparison | revisions src/HOL/Number_Theory/document/root.tex file | annotate | diff | comparison | revisions
--- a/CONTRIBUTORS	Sat Feb 02 15:52:14 2019 +0100
+++ b/CONTRIBUTORS	Mon Feb 04 12:16:03 2019 +0100
@@ -6,6 +6,10 @@
Contributions to this Isabelle version
--------------------------------------

+* February 2019: Manuel Eberl
+  Carmichael's function, primitive roots in residue rings, more properties
+  of the order in residue rings.
+
* January 2019: Andreas Lochbihler
New implementation for case_of_simps based on Code_Lazy's
pattern matching elimination algorithm.
--- a/NEWS	Sat Feb 02 15:52:14 2019 +0100
+++ b/NEWS	Mon Feb 04 12:16:03 2019 +0100
@@ -87,6 +87,9 @@

*** HOL ***

+* more material on residue rings in HOL-Number_Theory:
+Carmichael's function, primitive roots, more properties for "ord"
+
* the functions \<Union>, \<Inter>, \<Squnion>, \<Sqinter>
(not the corresponding binding operators) now have the same precedence
as any other prefix function symbol.
--- a/src/HOL/Algebra/Multiplicative_Group.thy	Sat Feb 02 15:52:14 2019 +0100
+++ b/src/HOL/Algebra/Multiplicative_Group.thy	Mon Feb 04 12:16:03 2019 +0100
@@ -136,7 +136,9 @@
shows "n > 0 \<and> n \<le> p"
using assms by (simp add: dvd_pos_nat dvd_imp_le)

-(* Deviates from the definition given in the library in number theory *)
+(* TODO FIXME: This is the "totient" function from HOL-Number_Theory, but since part of
+   HOL-Number_Theory depends on HOL-Algebra.Multiplicative_Group, there would be a cyclic
+   dependency. *)
definition phi' :: "nat => nat"
where "phi' m = card {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m}"

--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Sat Feb 02 15:52:14 2019 +0100
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Mon Feb 04 12:16:03 2019 +0100
@@ -1290,6 +1290,11 @@
with assms show "normalize x = normalize y" by (simp add: prod_mset_prime_factorization)
qed (rule prime_factorization_cong)

+lemma prime_factorization_eqI:
+  assumes "\<And>p. p \<in># P \<Longrightarrow> prime p" "prod_mset P = n"
+  shows   "prime_factorization n = P"
+  using prime_factorization_prod_mset_primes[of P] assms by simp
+
lemma prime_factorization_mult:
assumes "x \<noteq> 0" "y \<noteq> 0"
shows   "prime_factorization (x * y) = prime_factorization x + prime_factorization y"
@@ -1543,6 +1548,40 @@
with \<open>m \<le> n\<close> show thesis ..
qed

+lemma divide_out_primepow_ex:
+  assumes "n \<noteq> 0" "\<exists>p\<in>prime_factors n. P p"
+  obtains p k n' where "P p" "prime p" "p dvd n" "\<not>p dvd n'" "k > 0" "n = p ^ k * n'"
+proof -
+  from assms obtain p where p: "P p" "prime p" "p dvd n"
+    by auto
+  define k where "k = multiplicity p n"
+  define n' where "n' = n div p ^ k"
+  have n': "n = p ^ k * n'" "\<not>p dvd n'"
+    using assms p multiplicity_decompose[of n p]
+    by (auto simp: n'_def k_def multiplicity_dvd)
+  from n' p have "k > 0" by (intro Nat.gr0I) auto
+  with n' p that[of p n' k] show ?thesis by auto
+qed
+
+lemma divide_out_primepow:
+  assumes "n \<noteq> 0" "\<not>is_unit n"
+  obtains p k n' where "prime p" "p dvd n" "\<not>p dvd n'" "k > 0" "n = p ^ k * n'"
+  using divide_out_primepow_ex[OF assms(1), of "\<lambda>_. True"] prime_divisor_exists[OF assms] assms
+        prime_factorsI by metis
+
+lemma Ex_other_prime_factor:
+  assumes "n \<noteq> 0" and "\<not>(\<exists>k. normalize n = p ^ k)" "prime p"
+  shows   "\<exists>q\<in>prime_factors n. q \<noteq> p"
+proof (rule ccontr)
+  assume *: "\<not>(\<exists>q\<in>prime_factors n. q \<noteq> p)"
+  have "normalize n = (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n)"
+    using assms(1) by (intro prod_prime_factors [symmetric]) auto
+  also from * have "\<dots> = (\<Prod>p\<in>{p}. p ^ multiplicity p n)"
+    using assms(3) by (intro prod.mono_neutral_left) (auto simp: prime_factors_multiplicity)
+  finally have "normalize n = p ^ multiplicity p n" by auto
+  with assms show False by auto
+qed
+

subsection \<open>GCD and LCM computation with unique factorizations\<close>

--- a/src/HOL/Divides.thy	Sat Feb 02 15:52:14 2019 +0100
+++ b/src/HOL/Divides.thy	Mon Feb 04 12:16:03 2019 +0100
@@ -881,6 +881,21 @@
qed

+lemma mod_double_modulus:
+  assumes "m > 0" "x \<ge> 0"
+  shows   "x mod (2 * m) = x mod m \<or> x mod (2 * m) = x mod m + m"
+proof (cases "x mod (2 * m) < m")
+  case True
+  thus ?thesis using assms using divmod_digit_0(2)[of m x] by auto
+next
+  case False
+  hence *: "x mod (2 * m) - m = x mod m"
+    using assms by (intro divmod_digit_1) auto
+  hence "x mod (2 * m) = x mod m + m"
+    by (subst * [symmetric], subst le_add_diff_inverse2) (use False in auto)
+  thus ?thesis by simp
+qed
+
lemma fst_divmod:
"fst (divmod m n) = numeral m div numeral n"
by (simp add: divmod_def)
--- a/src/HOL/GCD.thy	Sat Feb 02 15:52:14 2019 +0100
+++ b/src/HOL/GCD.thy	Mon Feb 04 12:16:03 2019 +0100
@@ -682,6 +682,12 @@
by simp
qed

+lemma gcd_mono: "a dvd c \<Longrightarrow> b dvd d \<Longrightarrow> gcd a b dvd gcd c d"
+  by (simp add: gcd_dvdI1 gcd_dvdI2)
+
+lemma lcm_mono: "a dvd c \<Longrightarrow> b dvd d \<Longrightarrow> lcm a b dvd lcm c d"
+  by (simp add: dvd_lcmI1 dvd_lcmI2)
+
lemma dvd_productE:
assumes "p dvd a * b"
obtains x y where "p = x * y" "x dvd a" "y dvd b"
@@ -1081,6 +1087,29 @@
lemma Gcd_2 [simp]: "Gcd {a, b} = gcd a b"
by simp

+lemma Gcd_mono:
+  assumes "\<And>x. x \<in> A \<Longrightarrow> f x dvd g x"
+  shows   "(GCD x\<in>A. f x) dvd (GCD x\<in>A. g x)"
+proof (intro Gcd_greatest, safe)
+  fix x assume "x \<in> A"
+  hence "(GCD x\<in>A. f x) dvd f x"
+    by (intro Gcd_dvd) auto
+  also have "f x dvd g x"
+    using \<open>x \<in> A\<close> assms by blast
+  finally show "(GCD x\<in>A. f x) dvd \<dots>" .
+qed
+
+lemma Lcm_mono:
+  assumes "\<And>x. x \<in> A \<Longrightarrow> f x dvd g x"
+  shows   "(LCM x\<in>A. f x) dvd (LCM x\<in>A. g x)"
+proof (intro Lcm_least, safe)
+  fix x assume "x \<in> A"
+  hence "f x dvd g x" by (rule assms)
+  also have "g x dvd (LCM x\<in>A. g x)"
+    using \<open>x \<in> A\<close> by (intro dvd_Lcm) auto
+  finally show "f x dvd \<dots>" .
+qed
+
end


--- a/src/HOL/Number_Theory/Number_Theory.thy	Sat Feb 02 15:52:14 2019 +0100
+++ b/src/HOL/Number_Theory/Number_Theory.thy	Mon Feb 04 12:16:03 2019 +0100
@@ -2,7 +2,14 @@
section \<open>Comprehensive number theory\<close>

theory Number_Theory
-imports Fib Residues Eratosthenes Quadratic_Reciprocity Pocklington Prime_Powers
+imports
+  Fib
+  Residues
+  Eratosthenes
+  Pocklington
+  Prime_Powers
+  Residue_Primitive_Roots
begin

end
--- a/src/HOL/Number_Theory/Pocklington.thy	Sat Feb 02 15:52:14 2019 +0100
+++ b/src/HOL/Number_Theory/Pocklington.thy	Mon Feb 04 12:16:03 2019 +0100
@@ -1,5 +1,5 @@
(*  Title:      HOL/Number_Theory/Pocklington.thy
-    Author:     Amine Chaieb
+    Author:     Amine Chaieb, Manuel Eberl
*)

section \<open>Pocklington's Theorem for Primes\<close>
@@ -270,7 +270,7 @@
qed

-subsection \<open>Definition of the order of a number mod n (0 in non-coprime case)\<close>
+subsection \<open>Definition of the order of a number mod \<open>n\<close>\<close>

definition "ord n a = (if coprime n a then Least (\<lambda>d. d > 0 \<and> [a ^d = 1] (mod n)) else 0)"

@@ -439,6 +439,425 @@
qed
qed

+lemma ord_not_coprime [simp]: "\<not>coprime n a \<Longrightarrow> ord n a = 0"
+
+lemma ord_1 [simp]: "ord 1 n = 1"
+proof -
+  have "(LEAST k. k > 0) = (1 :: nat)"
+    by (rule Least_equality) auto
+  thus ?thesis by (simp add: ord_def)
+qed
+
+lemma ord_1_right [simp]: "ord (n::nat) 1 = 1"
+  using ord_divides[of 1 1 n] by simp
+
+lemma ord_Suc_0_right [simp]: "ord (n::nat) (Suc 0) = 1"
+  using ord_divides[of 1 1 n] by simp
+
+lemma ord_0_nat [simp]: "ord 0 (n :: nat) = (if n = 1 then 1 else 0)"
+proof -
+  have "(LEAST k. k > 0) = (1 :: nat)"
+    by (rule Least_equality) auto
+  thus ?thesis by (auto simp: ord_def)
+qed
+
+lemma ord_0_right_nat [simp]: "ord (n :: nat) 0 = (if n = 1 then 1 else 0)"
+proof -
+  have "(LEAST k. k > 0) = (1 :: nat)"
+    by (rule Least_equality) auto
+  thus ?thesis by (auto simp: ord_def)
+qed
+
+lemma ord_divides': "[a ^ d = Suc 0] (mod n) = (ord n a dvd d)"
+  using ord_divides[of a d n] by simp
+
+lemma ord_Suc_0 [simp]: "ord (Suc 0) n = 1"
+  using ord_1[where 'a = nat] by (simp del: ord_1)
+
+lemma ord_mod [simp]: "ord n (k mod n) = ord n k"
+  by (cases "n = 0") (auto simp add: ord_def cong_def power_mod)
+
+lemma ord_gt_0_iff [simp]: "ord (n::nat) x > 0 \<longleftrightarrow> coprime n x"
+  using ord_eq_0[of n x] by auto
+
+lemma ord_eq_Suc_0_iff: "ord n (x::nat) = Suc 0 \<longleftrightarrow> [x = 1] (mod n)"
+  using ord_divides[of x 1 n] by (auto simp: ord_divides')
+
+lemma ord_cong:
+  assumes "[k1 = k2] (mod n)"
+  shows   "ord n k1 = ord n k2"
+proof -
+  have "ord n (k1 mod n) = ord n (k2 mod n)"
+    by (simp only: assms[unfolded cong_def])
+  thus ?thesis by simp
+qed
+
+lemma ord_nat_code [code_unfold]:
+  "ord n a =
+     (if n = 0 then if a = 1 then 1 else 0 else
+        if coprime n a then Min (Set.filter (\<lambda>k. [a ^ k = 1] (mod n)) {0<..n}) else 0)"
+proof (cases "coprime n a \<and> n > 0")
+  case True
+  define A where "A = {k\<in>{0<..n}. [a ^ k = 1] (mod n)}"
+  define k where "k = (LEAST k. k > 0 \<and> [a ^ k = 1] (mod n))"
+  have totient: "totient n \<in> A"
+    using euler_theorem[of a n] True
+    by (auto simp: A_def coprime_commute intro!: Nat.gr0I totient_le)
+  moreover have "finite A" by (auto simp: A_def)
+  ultimately have *: "Min A \<in> A" and "\<forall>y. y \<in> A \<longrightarrow> Min A \<le> y"
+    by (auto intro: Min_in)
+
+  have "k > 0 \<and> [a ^ k = 1] (mod n)"
+    unfolding k_def by (rule LeastI[of _ "totient n"]) (use totient in \<open>auto simp: A_def\<close>)
+  moreover have "k \<le> totient n"
+    unfolding k_def by (intro Least_le) (use totient in \<open>auto simp: A_def\<close>)
+  ultimately have "k \<in> A" using totient_le[of n] by (auto simp: A_def)
+  hence "Min A \<le> k" by (intro Min_le) (auto simp: \<open>finite A\<close>)
+  moreover from * have "k \<le> Min A"
+    unfolding k_def by (intro Least_le) (auto simp: A_def)
+  ultimately show ?thesis using True by (simp add: ord_def k_def A_def Set.filter_def)
+qed auto
+
+theorem ord_modulus_mult_coprime:
+  fixes x :: nat
+  assumes "coprime m n"
+  shows   "ord (m * n) x = lcm (ord m x) (ord n x)"
+proof (intro dvd_antisym)
+  have "[x ^ lcm (ord m x) (ord n x) = 1] (mod (m * n))"
+    using assms by (intro coprime_cong_mult_nat assms) (auto simp: ord_divides')
+  thus "ord (m * n) x dvd lcm (ord m x) (ord n x)"
+next
+  show "lcm (ord m x) (ord n x) dvd ord (m * n) x"
+  proof (intro lcm_least)
+    show "ord m x dvd ord (m * n) x"
+      using cong_modulus_mult_nat[of "x ^ ord (m * n) x" 1 m n] assms
+    show "ord n x dvd ord (m * n) x"
+      using cong_modulus_mult_nat[of "x ^ ord (m * n) x" 1 n m] assms
+      by (simp add: ord_divides' mult.commute)
+  qed
+qed
+
+corollary ord_modulus_prod_coprime:
+  assumes "finite A" "\<And>i j. i \<in> A \<Longrightarrow> j \<in> A \<Longrightarrow> i \<noteq> j \<Longrightarrow> coprime (f i) (f j)"
+  shows   "ord (\<Prod>i\<in>A. f i :: nat) x = (LCM i\<in>A. ord (f i) x)"
+  using assms by (induction A rule: finite_induct)
+                 (simp, simp, subst ord_modulus_mult_coprime, auto intro!: prod_coprime_right)
+
+lemma ord_power_aux:
+  fixes m x k a :: nat
+  defines "l \<equiv> ord m a"
+  shows   "ord m (a ^ k) * gcd k l = l"
+proof (rule dvd_antisym)
+  have "[a ^ lcm k l = 1] (mod m)"
+    unfolding ord_divides by (simp add: l_def)
+  also have "lcm k l = k * (l div gcd k l)"
+    by (simp add: lcm_nat_def div_mult_swap)
+  finally have "ord m (a ^ k) dvd l div gcd k l"
+    unfolding ord_divides [symmetric] by (simp add: power_mult [symmetric])
+  thus "ord m (a ^ k) * gcd k l dvd l"
+    by (cases "l = 0") (auto simp: dvd_div_iff_mult)
+
+  have "[(a ^ k) ^ ord m (a ^ k) = 1] (mod m)"
+    by (rule ord)
+  also have "(a ^ k) ^ ord m (a ^ k) = a ^ (k * ord m (a ^ k))"
+  finally have "ord m a dvd k * ord m (a ^ k)"
+  hence "l dvd gcd (k * ord m (a ^ k)) (l * ord m (a ^ k))"
+    by (intro gcd_greatest dvd_triv_left) (auto simp: l_def ord_divides')
+  also have "gcd (k * ord m (a ^ k)) (l * ord m (a ^ k)) = ord m (a ^ k) * gcd k l"
+    by (subst gcd_mult_distrib_nat) (auto simp: mult_ac)
+  finally show "l dvd ord m (a ^ k) * gcd k l" .
+qed
+
+theorem ord_power: "coprime m a \<Longrightarrow> ord m (a ^ k :: nat) = ord m a div gcd k (ord m a)"
+  using ord_power_aux[of m a k] by (metis div_mult_self_is_m gcd_pos_nat ord_eq_0)
+
+lemma inj_power_mod:
+  assumes "coprime n (a :: nat)"
+  shows   "inj_on (\<lambda>k. a ^ k mod n) {..<ord n a}"
+proof
+  fix k l assume *: "k \<in> {..<ord n a}" "l \<in> {..<ord n a}" "a ^ k mod n = a ^ l mod n"
+  have "k = l" if "k < l" "l < ord n a" "[a ^ k = a ^ l] (mod n)" for k l
+  proof -
+    have "l = k + (l - k)" using that by simp
+    also have "a ^ \<dots> = a ^ k * a ^ (l - k)"
+    also have "[\<dots> = a ^ l * a ^ (l - k)] (mod n)"
+      using that by (intro cong_mult) auto
+    finally have "[a ^ l * a ^ (l - k) = a ^ l * 1] (mod n)"
+    with assms have "[a ^ (l - k) = 1] (mod n)"
+      by (subst (asm) cong_mult_lcancel_nat) (auto simp: coprime_commute)
+    hence "ord n a dvd l - k"
+    from dvd_imp_le[OF this] and \<open>l < ord n a\<close> have "l - k = 0"
+      by (cases "l - k = 0") auto
+    with \<open>k < l\<close> show "k = l" by simp
+  qed
+  from this[of k l] and this[of l k] and * show "k = l"
+    by (cases k l rule: linorder_cases) (auto simp: cong_def)
+qed
+
+lemma ord_eq_2_iff: "ord n (x :: nat) = 2 \<longleftrightarrow> [x \<noteq> 1] (mod n) \<and> [x\<^sup>2 = 1] (mod n)"
+proof
+  assume x: "[x \<noteq> 1] (mod n) \<and> [x\<^sup>2 = 1] (mod n)"
+  hence "coprime n x"
+    by (metis coprime_commute lucas_coprime_lemma zero_neq_numeral)
+  with x have "ord n x dvd 2" "ord n x \<noteq> 1" "ord n x > 0"
+    by (auto simp: ord_divides' ord_eq_Suc_0_iff)
+  thus "ord n x = 2" by (auto dest!: dvd_imp_le simp del: ord_gt_0_iff)
+qed (use ord_divides[of _ 2] ord_divides[of _ 1] in auto)
+
+lemma square_mod_8_eq_1_iff: "[x\<^sup>2 = 1] (mod 8) \<longleftrightarrow> odd (x :: nat)"
+proof -
+  have "[x\<^sup>2 = 1] (mod 8) \<longleftrightarrow> ((x mod 8)\<^sup>2 mod 8 = 1)"
+    by (simp add: power_mod cong_def)
+  also have "\<dots> \<longleftrightarrow> x mod 8 \<in> {1, 3, 5, 7}"
+  proof
+    assume x: "(x mod 8)\<^sup>2 mod 8 = 1"
+    have "x mod 8 \<in> {..<8}" by simp
+    also have "{..<8} = {0, 1, 2, 3, 4, 5, 6, 7::nat}"
+      by (simp add: lessThan_nat_numeral lessThan_Suc insert_commute)
+    finally have x_cases: "x mod 8 \<in> {0, 1, 2, 3, 4, 5, 6, 7}" .
+    from x have "x mod 8 \<notin> {0, 2, 4, 6}"
+      using x by (auto intro: Nat.gr0I)
+    with x_cases show "x mod 8 \<in> {1, 3, 5, 7}" by simp
+  qed auto
+  also have "\<dots> \<longleftrightarrow> odd (x mod 8)"
+    by (auto elim!: oddE)
+  also have "\<dots> \<longleftrightarrow> odd x"
+    by presburger
+  finally show ?thesis .
+qed
+
+lemma ord_twopow_aux:
+  assumes "k \<ge> 3" and "odd (x :: nat)"
+  shows   "[x ^ (2 ^ (k - 2)) = 1] (mod (2 ^ k))"
+  using assms(1)
+proof (induction k rule: dec_induct)
+  case base
+  from assms have "[x\<^sup>2 = 1] (mod 8)"
+    by (subst square_mod_8_eq_1_iff) auto
+  thus ?case by simp
+next
+  case (step k)
+  define k' where "k' = k - 2"
+  have k: "k = Suc (Suc k')"
+    using \<open>k \<ge> 3\<close> by (simp add: k'_def)
+  from \<open>k \<ge> 3\<close> have "2 * k \<ge> Suc k" by presburger
+
+  from \<open>odd x\<close> have "x > 0" by (intro Nat.gr0I) auto
+  from step.IH have "2 ^ k dvd (x ^ (2 ^ (k - 2)) - 1)"
+    by (rule cong_to_1_nat)
+  then obtain t where "x ^ (2 ^ (k - 2)) - 1 = t * 2 ^ k"
+    by auto
+  hence "x ^ (2 ^ (k - 2)) = t * 2 ^ k + 1"
+  hence "(x ^ (2 ^ (k - 2))) ^ 2 = (t * 2 ^ k + 1) ^ 2"
+    by (rule arg_cong)
+  hence "[(x ^ (2 ^ (k - 2))) ^ 2 = (t * 2 ^ k + 1) ^ 2] (mod (2 ^ Suc k))"
+    by simp
+  also have "(x ^ (2 ^ (k - 2))) ^ 2 = x ^ (2 ^ (k - 1))"
+    by (simp_all add: power_even_eq[symmetric] power_mult k )
+  also have "(t * 2 ^ k + 1) ^ 2 = t\<^sup>2 * 2 ^ (2 * k) + t * 2 ^ Suc k + 1"
+    by (subst power2_eq_square)
+       (auto simp: algebra_simps k power2_eq_square[of t]
+  also have "[\<dots> = 0 + 0 + 1] (mod 2 ^ Suc k)"
+    using \<open>2 * k \<ge> Suc k\<close>
+       (auto simp: cong_0_iff intro: dvd_mult[OF le_imp_power_dvd] simp del: power_Suc)
+  finally show ?case by simp
+qed
+
+lemma ord_twopow_3_5:
+  assumes "k \<ge> 3" "x mod 8 \<in> {3, 5 :: nat}"
+  shows   "ord (2 ^ k) x = 2 ^ (k - 2)"
+  using assms(1)
+proof (induction k rule: less_induct)
+  have "x mod 8 = 3 \<or> x mod 8 = 5" using assms by auto
+  hence "odd x" by presburger
+  case (less k)
+  from \<open>k \<ge> 3\<close> consider "k = 3" | "k = 4" | "k \<ge> 5" by force
+  thus ?case
+  proof cases
+    case 1
+    thus ?thesis using assms
+      by (auto simp: ord_eq_2_iff cong_def simp flip: power_mod[of x])
+  next
+    case 2
+    from assms have "x mod 8 = 3 \<or> x mod 8 = 5" by auto
+    hence x': "x mod 16 = 3 \<or> x mod 16 = 5 \<or> x mod 16 = 11 \<or> x mod 16 = 13"
+      using mod_double_modulus[of 8 x] by auto
+    hence "[x ^ 4 = 1] (mod 16)" using assms
+      by (auto simp: cong_def simp flip: power_mod[of x])
+    hence "ord 16 x dvd 2\<^sup>2" by (simp add: ord_divides')
+    then obtain l where l: "ord 16 x = 2 ^ l" "l \<le> 2"
+      by (subst (asm) divides_primepow_nat) auto
+
+    have "[x ^ 2 \<noteq> 1] (mod 16)"
+      using x' by (auto simp: cong_def simp flip: power_mod[of x])
+    hence "\<not>ord 16 x dvd 2" by (simp add: ord_divides')
+    with l have "l = 2"
+      using le_imp_power_dvd[of l 1 2] by (cases "l \<le> 1") auto
+    with l show ?thesis by (simp add: \<open>k = 4\<close>)
+  next
+    case 3
+    define k' where "k' = k - 2"
+    have k': "k' \<ge> 2" and [simp]: "k = Suc (Suc k')"
+      using 3 by (simp_all add: k'_def)
+    have IH: "ord (2 ^ k') x = 2 ^ (k' - 2)" "ord (2 ^ Suc k') x = 2 ^ (k' - 1)"
+      using less.IH[of k'] less.IH[of "Suc k'"] 3 by simp_all
+    from IH have cong: "[x ^ (2 ^ (k' - 2)) = 1] (mod (2 ^ k'))"
+    have notcong: "[x ^ (2 ^ (k' - 2)) \<noteq> 1] (mod (2 ^ Suc k'))"
+    proof
+      assume "[x ^ (2 ^ (k' - 2)) = 1] (mod (2 ^ Suc k'))"
+      hence "ord (2 ^ Suc k') x dvd 2 ^ (k' - 2)"
+      also have "ord (2 ^ Suc k') x = 2 ^ (k' - 1)"
+        using IH by simp
+      finally have "k' - 1 \<le> k' - 2"
+        by (rule power_dvd_imp_le) auto
+      with \<open>k' \<ge> 2\<close> show False by simp
+    qed
+
+    have "2 ^ k' + 1 < 2 ^ k' + (2 ^ k' :: nat)"
+      using one_less_power[of "2::nat" k'] k' by (intro add_strict_left_mono) auto
+    with cong notcong have cong': "x ^ (2 ^ (k' - 2)) mod 2 ^ Suc k' = 1 + 2 ^ k'"
+      using mod_double_modulus[of "2 ^ k'" "x ^ 2 ^ (k' - 2)"] k' by (auto simp: cong_def)
+
+    hence "x ^ (2 ^ (k' - 2)) mod 2 ^ k = 1 + 2 ^ k' \<or>
+           x ^ (2 ^ (k' - 2)) mod 2 ^ k = 1 + 2 ^ k' + 2 ^ Suc k'"
+      using mod_double_modulus[of "2 ^ Suc k'" "x ^ 2 ^ (k' - 2)"] by auto
+    hence eq: "[x ^ 2 ^ (k' - 1) = 1 + 2 ^ (k - 1)] (mod 2 ^ k)"
+    proof
+      assume *: "x ^ (2 ^ (k' - 2)) mod (2 ^ k) = 1 + 2 ^ k'"
+      have "[x ^ (2 ^ (k' - 2)) = x ^ (2 ^ (k' - 2)) mod 2 ^ k] (mod 2 ^ k)"
+        by simp
+      also have "[x ^ (2 ^ (k' - 2)) mod (2 ^ k) = 1 + 2 ^ k'] (mod 2 ^ k)"
+        by (subst *) auto
+      finally have "[(x ^ 2 ^ (k' - 2)) ^ 2 = (1 + 2 ^ k') ^ 2] (mod 2 ^ k)"
+        by (rule cong_pow)
+      hence "[x ^ 2 ^ Suc (k' - 2) = (1 + 2 ^ k') ^ 2] (mod 2 ^ k)"
+        by (simp add: power_mult [symmetric] power_Suc2 [symmetric] del: power_Suc)
+      also have "Suc (k' - 2) = k' - 1"
+        using k' by simp
+      also have "(1 + 2 ^ k' :: nat)\<^sup>2 = 1 + 2 ^ (k - 1) + 2 ^ (2 * k')"
+      also have "(2 ^ k :: nat) dvd 2 ^ (2 * k')"
+        using k' by (intro le_imp_power_dvd) auto
+      hence "[1 + 2 ^ (k - 1) + 2 ^ (2 * k') = 1 + 2 ^ (k - 1) + (0 :: nat)] (mod 2 ^ k)"
+        by (intro cong_add) (auto simp: cong_0_iff)
+      finally show "[x ^ 2 ^ (k' - 1) = 1 + 2 ^ (k - 1)] (mod 2 ^ k)"
+        by simp
+    next
+      assume *: "x ^ (2 ^ (k' - 2)) mod 2 ^ k = 1 + 2 ^ k' + 2 ^ Suc k'"
+      have "[x ^ (2 ^ (k' - 2)) = x ^ (2 ^ (k' - 2)) mod 2 ^ k] (mod 2 ^ k)"
+        by simp
+      also have "[x ^ (2 ^ (k' - 2)) mod (2 ^ k) = 1 + 3 * 2 ^ k'] (mod 2 ^ k)"
+        by (subst *) auto
+      finally have "[(x ^ 2 ^ (k' - 2)) ^ 2 = (1 + 3 * 2 ^ k') ^ 2] (mod 2 ^ k)"
+        by (rule cong_pow)
+      hence "[x ^ 2 ^ Suc (k' - 2) = (1 + 3 * 2 ^ k') ^ 2] (mod 2 ^ k)"
+        by (simp add: power_mult [symmetric] power_Suc2 [symmetric] del: power_Suc)
+      also have "Suc (k' - 2) = k' - 1"
+        using k' by simp
+      also have "(1 + 3 * 2 ^ k' :: nat)\<^sup>2 = 1 + 2 ^ (k - 1) + 2 ^ k + 9 * 2 ^ (2 * k')"
+      also have "(2 ^ k :: nat) dvd 9 * 2 ^ (2 * k')"
+        using k' by (intro dvd_mult le_imp_power_dvd) auto
+      hence "[1 + 2 ^ (k - 1) + 2 ^ k + 9 * 2 ^ (2 * k') = 1 + 2 ^ (k - 1) + 0 + (0 :: nat)]
+               (mod 2 ^ k)"
+        by (intro cong_add) (auto simp: cong_0_iff)
+      finally show "[x ^ 2 ^ (k' - 1) = 1 + 2 ^ (k - 1)] (mod 2 ^ k)"
+        by simp
+    qed
+
+    have notcong': "[x ^ 2 ^ (k - 3) \<noteq> 1] (mod 2 ^ k)"
+    proof
+      assume "[x ^ 2 ^ (k - 3) = 1] (mod 2 ^ k)"
+      hence "[x ^ 2 ^ (k' - 1) - x ^ 2 ^ (k' - 1) = 1 + 2 ^ (k - 1) - 1] (mod 2 ^ k)"
+        by (intro cong_diff_nat eq) auto
+      hence "[2 ^ (k - 1) = (0 :: nat)] (mod 2 ^ k)"
+      hence "2 ^ k dvd 2 ^ (k - 1)"
+      hence "k \<le> k - 1"
+        by (rule power_dvd_imp_le) auto
+      thus False by simp
+    qed
+
+    have "[x ^ 2 ^ (k - 2) = 1] (mod 2 ^ k)"
+      using ord_twopow_aux[of k x] \<open>odd x\<close> \<open>k \<ge> 3\<close> by simp
+    hence "ord (2 ^ k) x dvd 2 ^ (k - 2)"
+    then obtain l where l: "l \<le> k - 2" "ord (2 ^ k) x = 2 ^ l"
+      using divides_primepow_nat[of 2 "ord (2 ^ k) x" "k - 2"] by auto
+
+    from notcong' have "\<not>ord (2 ^ k) x dvd 2 ^ (k - 3)"
+    with l have "l = k - 2"
+      using le_imp_power_dvd[of l "k - 3" 2] by (cases "l \<le> k - 3") auto
+    with l show ?thesis by simp
+  qed
+qed
+
+lemma ord_4_3 [simp]: "ord 4 (3::nat) = 2"
+proof -
+  have "[3 ^ 2 = (1 :: nat)] (mod 4)"
+  hence "ord 4 (3::nat) dvd 2"
+    by (subst (asm) ord_divides) auto
+  hence "ord 4 (3::nat) \<le> 2"
+    by (intro dvd_imp_le) auto
+  moreover have "ord 4 (3::nat) \<noteq> 1"
+    by (auto simp: ord_eq_Suc_0_iff cong_def)
+  moreover have "ord 4 (3::nat) \<noteq> 0"
+    by (auto simp: gcd_non_0_nat coprime_iff_gcd_eq_1)
+  ultimately show "ord 4 (3 :: nat) = 2"
+    by linarith
+qed
+
+lemma elements_with_ord_1: "n > 0 \<Longrightarrow> {x\<in>totatives n. ord n x = Suc 0} = {1}"
+  by (auto simp: ord_eq_Suc_0_iff cong_def totatives_less)
+
+lemma residue_prime_has_primroot:
+  fixes p :: nat
+  assumes "prime p"
+  shows "\<exists>a\<in>totatives p. ord p a = p - 1"
+proof -
+  from residue_prime_mult_group_has_gen[OF assms]
+    obtain a where a: "a \<in> {1..p-1}" "{1..p-1} = {a ^ i mod p |i. i \<in> UNIV}" by blast
+  from a have "coprime p a"
+    using a assms by (intro prime_imp_coprime) (auto dest: dvd_imp_le)
+  with a(1) have "a \<in> totatives p" by (auto simp: totatives_def coprime_commute)
+
+  have "p - 1 = card {1..p-1}" by simp
+  also have "{1..p-1} = {a ^ i mod p |i. i \<in> UNIV}" by fact
+  also have "{a ^ i mod p |i. i \<in> UNIV} = (\<lambda>i. a ^ i mod p)  {..<ord p a}"
+  proof (intro equalityI subsetI)
+    fix x assume "x \<in> {a ^ i mod p |i. i \<in> UNIV}"
+    then obtain i where [simp]: "x = a ^ i mod p" by auto
+
+    have "[a ^ i = a ^ (i mod ord p a)] (mod p)"
+      using \<open>coprime p a\<close> by (subst order_divides_expdiff) auto
+    hence "\<exists>j. a ^ i mod p = a ^ j mod p \<and> j < ord p a"
+      using \<open>coprime p a\<close> by (intro exI[of _ "i mod ord p a"]) (auto simp: cong_def)
+    thus "x \<in> (\<lambda>i. a ^ i mod p)  {..<ord p a}"
+      by auto
+  qed auto
+  also have "card \<dots> = ord p a"
+    using inj_power_mod[OF \<open>coprime p a\<close>] by (subst card_image) auto
+  finally show ?thesis using \<open>a \<in> totatives p\<close>
+    by auto
+qed
+
+

subsection \<open>Another trivial primality characterization\<close>

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Number_Theory/Residue_Primitive_Roots.thy	Mon Feb 04 12:16:03 2019 +0100
@@ -0,0 +1,1152 @@
+(*
+  File:      HOL/Number_Theory/Residue_Primitive_Roots.thy
+  Author:    Manuel Eberl
+
+  Primitive roots in residue rings: Definition and existence criteria
+*)
+section \<open>Primitive roots in residue rings and Carmichael's function\<close>
+theory Residue_Primitive_Roots
+  imports Pocklington
+begin
+
+text \<open>
+  This theory develops the notions of primitive roots (generators) in residue rings. It also
+  provides a definition and all the basic properties of Carmichael's function $\lambda(n)$, which
+  is strongly related to this. The proofs mostly follow Apostol's presentation
+\<close>
+
+subsection \<open>Primitive roots in residue rings\<close>
+
+text \<open>
+  A primitive root of a residue ring modulo \<open>n\<close> is an element \<open>g\<close> that \<^emph>\<open>generates\<close> the
+  ring, i.\,e.\ such that for each \<open>x\<close> coprime to \<open>n\<close> there exists an \<open>i\<close> such that $x = g^i$.
+  A simpler definition is that \<open>g\<close> must have the same order as the cardinality of the
+  multiplicative group, which is $\varphi(n)$.
+
+  Note that for convenience, this definition does \<^emph>\<open>not\<close> demand \<open>g < n\<close>.
+\<close>
+inductive residue_primroot :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
+  "n > 0 \<Longrightarrow> coprime n g \<Longrightarrow> ord n g = totient n \<Longrightarrow> residue_primroot n g"
+
+lemma residue_primroot_def [code]:
+  "residue_primroot n x \<longleftrightarrow> n > 0 \<and> coprime n x \<and> ord n x = totient n"
+
+lemma not_residue_primroot_0 [simp]: "~residue_primroot 0 x"
+  by (auto simp: residue_primroot_def)
+
+lemma residue_primroot_mod [simp]: "residue_primroot n (x mod n) = residue_primroot n x"
+  by (cases "n = 0") (simp_all add: residue_primroot_def)
+
+lemma residue_primroot_cong:
+  assumes "[x = x'] (mod n)"
+  shows   "residue_primroot n x = residue_primroot n x'"
+proof -
+  have "residue_primroot n x = residue_primroot n (x mod n)"
+    by simp
+  also have "x mod n = x' mod n"
+    using assms by (simp add: cong_def)
+  also have "residue_primroot n (x' mod n) = residue_primroot n x'"
+    by simp
+  finally show ?thesis .
+qed
+
+lemma not_residue_primroot_0_right [simp]: "residue_primroot n 0 \<longleftrightarrow> n = 1"
+  by (auto simp: residue_primroot_def)
+
+lemma residue_primroot_1_iff: "residue_primroot n (Suc 0) \<longleftrightarrow> n \<in> {1, 2}"
+proof
+  assume *: "residue_primroot n (Suc 0)"
+  with totient_gt_1[of n] have "n \<le> 2" by (cases "n \<le> 2") (auto simp: residue_primroot_def)
+  hence "n \<in> {0, 1, 2}" by auto
+  thus "n \<in> {1, 2}" using * by (auto simp: residue_primroot_def)
+qed (auto simp: residue_primroot_def)
+
+
+subsection \<open>Primitive roots modulo a prime\<close>
+
+text \<open>
+  For prime \<open>p\<close>, we now analyse the number of elements in the ring $\mathbb{Z}/p\mathbb{Z}$
+  whose order is precisely \<open>d\<close> for each \<open>d\<close>.
+\<close>
+context
+  fixes n :: nat and \<psi>
+  assumes n: "n > 1"
+  defines "\<psi> \<equiv> (\<lambda>d. card {x\<in>totatives n. ord n x = d})"
+begin
+
+lemma elements_with_ord_restrict_totatives:
+  "d > 0 \<Longrightarrow> {x\<in>{..<n}. ord n x = d} = {x\<in>totatives n. ord n x = d}"
+  using n by (auto simp: totatives_def coprime_commute intro!: Nat.gr0I le_neq_trans)
+
+lemma prime_elements_with_ord:
+  assumes "\<psi> d \<noteq> 0" and "prime n"
+      and a: "a \<in> totatives n" "ord n a = d" "a \<noteq> 1"
+  shows   "inj_on (\<lambda>k. a ^ k mod n) {..<d}"
+    and   "{x\<in>{..<n}. [x ^ d = 1] (mod n)} = (\<lambda>k. a ^ k mod n)  {..<d}"
+    and   "bij_betw (\<lambda>k. a ^ k mod n) (totatives d) {x\<in>{..<n}. ord n x = d}"
+proof -
+  show inj: "inj_on (\<lambda>k. a ^ k mod n) {..<d}"
+    using inj_power_mod[of n a] a by (auto simp: totatives_def coprime_commute)
+  from a have "d > 0" by (auto simp: totatives_def coprime_commute)
+  moreover have "d \<noteq> 1" using a n
+    by (auto simp: ord_eq_Suc_0_iff totatives_less cong_def)
+  ultimately have d: "d > 1" by simp
+
+  have *: "(\<lambda>k. a ^ k mod n)  {..<d} = {x\<in>{..<n}. [x ^ d = 1] (mod n)}"
+  proof (rule card_seteq)
+    have "card {x\<in>{..<n}. [x ^ d = 1] (mod n)} \<le> d"
+      using assms a by (intro roots_mod_prime_bound) (auto simp: totatives_def coprime_commute)
+    also have "\<dots> = card ((\<lambda>k. a ^ k mod n)  {..<d})"
+      using inj by (subst card_image) auto
+    finally show "card {x \<in> {..<n}. [x ^ d = 1] (mod n)} \<le> \<dots>" .
+  next
+    show "(\<lambda>k. a ^ k mod n)  {..<d} \<subseteq> {x \<in> {..<n}. [x ^ d = 1] (mod n)}"
+    proof safe
+      fix k assume "k < d"
+      have "[(a ^ d) ^ k = 1 ^ k] (mod n)"
+        by (intro cong_pow) (use a in \<open>auto simp: ord_divides'\<close>)
+      thus "[(a ^ k mod n) ^ d = 1] (mod n)"
+        by (simp add: power_mult [symmetric] cong_def power_mod mult.commute)
+    qed (use \<open>prime n\<close> in \<open>auto dest: prime_gt_1_nat\<close>)
+  qed auto
+  thus "{x\<in>{..<n}. [x ^ d = 1] (mod n)} = (\<lambda>k. a ^ k mod n)  {..<d}" ..
+
+  show "bij_betw (\<lambda>k. a ^ k mod n) (totatives d) {x\<in>{..<n}. ord n x = d}"
+    unfolding bij_betw_def
+  proof (intro conjI inj_on_subset[OF inj] equalityI subsetI)
+    fix b assume "b \<in> (\<lambda>k. a ^ k mod n)  totatives d"
+    then obtain k where "b = a ^ k mod n" "k \<in> totatives d" by auto
+    thus "b \<in> {b \<in> {..<n}. ord n b = d}"
+      using n a by (simp add: ord_power totatives_def coprime_commute)
+  next
+    fix b assume "b \<in> {x \<in> {..<n}. ord n x = d}"
+    hence b: "ord n b = d" "b < n" by auto
+    with d have "coprime n b" using ord_eq_0[of n b] by auto
+    from b have "b \<in> {x\<in>{..<n}. [x ^ d = 1] (mod n)}"
+      by (auto simp: ord_divides')
+    with * obtain k where k: "k < d" "b = a ^ k mod n"
+      by blast
+    with b(2) n a d have "d div gcd k d = ord n b"
+      using \<open>coprime n b\<close> by (auto simp: ord_power)
+    also have "ord n b = d" by (simp add: b)
+    finally have "coprime k d"
+      unfolding coprime_iff_gcd_eq_1 using d a by (subst (asm) div_eq_dividend_iff) auto
+    with k b d have "k \<in> totatives d" by (auto simp: totatives_def intro!: Nat.gr0I)
+    with k show "b \<in> (\<lambda>k. a ^ k mod n)  totatives d" by blast
+  qed (use d n in \<open>auto simp: totatives_less\<close>)
+qed
+
+lemma prime_card_elements_with_ord:
+  assumes "\<psi> d \<noteq> 0" and "prime n"
+  shows   "\<psi> d = totient d"
+proof (cases "d = 1")
+  case True
+  have "\<psi> 1 = 1"
+    using elements_with_ord_1[of n] n by (simp add: \<psi>_def)
+  thus ?thesis using True by simp
+next
+  case False
+  from assms obtain a where a: "a \<in> totatives n" "ord n a = d"
+    by (auto simp: \<psi>_def)
+  from a have "d > 0" by (auto intro!: Nat.gr0I simp: ord_eq_0 totatives_def coprime_commute)
+  from a and False have "a \<noteq> 1" by auto
+  from bij_betw_same_card[OF prime_elements_with_ord(3)[OF assms a this]] show "\<psi> d = totient d"
+    using elements_with_ord_restrict_totatives[of d] False a \<open>d > 0\<close>
+    by (simp add: \<psi>_def totient_def)
+qed
+
+lemma prime_sum_card_elements_with_ord_eq_totient:
+  "(\<Sum>d | d dvd totient n. \<psi> d) = totient n"
+proof -
+  have "totient n = card (totatives n)"
+  also have "totatives n = (\<Union>d\<in>{d. d dvd totient n}. {x\<in>totatives n. ord n x = d})"
+    by (force simp: order_divides_totient totatives_def coprime_commute)
+  also have "card \<dots> = (\<Sum>d | d dvd totient n. \<psi> d)"
+    unfolding \<psi>_def using n by (subst card_UN_disjoint) (auto intro!: finite_divisors_nat)
+  finally show ?thesis ..
+qed
+
+text \<open>
+  We can now show that the number of elements of order \<open>d\<close> is $\varphi(d)$ if $d\mid p - 1$
+  and 0 otherwise.
+\<close>
+theorem prime_card_elements_with_ord_eq_totient:
+  assumes "prime n"
+  shows   "\<psi> d = (if d dvd n - 1 then totient d else 0)"
+proof (cases "d dvd totient n")
+  case False
+  thus ?thesis using order_divides_totient[of n] assms
+    by (auto simp: \<psi>_def totient_prime totatives_def coprime_commute[of n])
+next
+  case True
+  have "\<psi> d = totient d"
+  proof (rule ccontr)
+    assume neq: "\<psi> d \<noteq> totient d"
+    have le: "\<psi> d \<le> totient d" if "d dvd totient n" for d
+      using prime_card_elements_with_ord[of d] assms by (cases "\<psi> d = 0") auto
+    from neq and le[of d] and True have less: "\<psi> d < totient d" by auto
+
+    have "totient n = (\<Sum>d | d dvd totient n. \<psi> d)"
+      using prime_sum_card_elements_with_ord_eq_totient ..
+    also have "\<dots> < (\<Sum>d | d dvd totient n. totient d)"
+      by (rule sum_strict_mono_ex1)
+         (use n le less assms True in \<open>auto intro!: finite_divisors_nat\<close>)
+    also have "\<dots> = totient n"
+      using totient_divisor_sum .
+    finally show False by simp
+  qed
+  with True show ?thesis using assms by (simp add: totient_prime)
+qed
+
+text \<open>
+  As a corollary, we get that the number of primitive roots modulo a prime \<open>p\<close> is
+  $\varphi(p - 1)$. Since this number is positive, we also get that there \<^emph>\<open>is\<close> at least
+  one primitive root modulo \<open>p\<close>.
+\<close>
+lemma
+  assumes "prime n"
+  shows   prime_card_primitive_roots:  "card {x\<in>totatives n. ord n x = n - 1} = totient (n - 1)"
+                                       "card {x\<in>{..<n}. ord n x = n - 1} = totient (n - 1)"
+  and     prime_primitive_root_exists: "\<exists>x. residue_primroot n x"
+proof -
+  show *: "card {x\<in>totatives n. ord n x = n - 1} = totient (n - 1)"
+    using prime_card_elements_with_ord_eq_totient[of "n - 1"] assms
+    by (auto simp: totient_prime \<psi>_def)
+  thus "card {x\<in>{..<n}. ord n x = n - 1} = totient (n - 1)"
+    using assms n elements_with_ord_restrict_totatives[of "n - 1"] by simp
+
+  note *
+  also have "totient (n - 1) > 0" using n by auto
+  finally show "\<exists>x. residue_primroot n x" using assms prime_gt_1_nat[of n]
+    by (subst (asm) card_gt_0_iff)
+       (auto simp: residue_primroot_def totient_prime totatives_def coprime_commute)
+qed
+
+end
+
+
+subsection \<open>Primitive roots modulo powers of an odd prime\<close>
+
+text \<open>
+  Any primitive root \<open>g\<close> modulo an odd prime \<open>p\<close> is also a primitive root modulo $p^k$ for all
+  $k > 0$ if $[g^{p - 1} \neq 1]\ (\text{mod}\ p^2)$. To show this, we first need the
+  following lemma.
+\<close>
+lemma residue_primroot_power_prime_power_neq_1:
+  assumes "k \<ge> 2"
+  assumes p: "prime p" "odd p" and "residue_primroot p g" and "[g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
+  shows   "[g ^ totient (p ^ (k - 1)) \<noteq> 1] (mod (p ^ k))"
+  using assms(1)
+proof (induction k rule: dec_induct)
+  case base
+  thus ?case using assms by (simp add: totient_prime)
+next
+  case (step k)
+  from p have "p > 2"
+    using prime_gt_1_nat[of p] by (cases "p = 2") auto
+  from assms have g: "g > 0" by (auto intro!: Nat.gr0I)
+  have "[g ^ totient (p ^ (k - 1)) = 1] (mod p ^ (k - 1))"
+    using assms by (intro euler_theorem)
+                   (auto simp: residue_primroot_def totatives_def coprime_commute)
+  from cong_to_1_nat[OF this]
+    obtain t where *: "g ^ totient (p ^ (k - 1)) - 1 = p ^ (k - 1) * t" by auto
+  have t: "g ^ totient (p ^ (k - 1)) = p ^ (k - 1) * t + 1"
+    using g by (subst * [symmetric]) auto
+
+  have "\<not>p dvd t"
+  proof
+    assume "p dvd t"
+    then obtain q where [simp]: "t = p * q" by auto
+    from t have "g ^ totient (p ^ (k - 1)) = p ^ k * q + 1"
+      using \<open>k \<ge> 2\<close> by (cases k) auto
+    hence "[g ^ totient (p ^ (k - 1)) = p ^ k * q + 1] (mod p ^ k)"
+      by simp
+    also have "[p ^ k * q + 1 = 0 * q + 1] (mod p ^ k)"
+      by (intro cong_add cong_mult) (auto simp: cong_0_iff)
+    finally have "[g ^ totient (p ^ (k - 1)) = 1] (mod p ^ k)"
+      by simp
+    with step.IH show False by contradiction
+  qed
+
+  from t have "(g ^ totient (p ^ (k - 1))) ^ p = (p ^ (k - 1) * t + 1) ^ p"
+    by (rule arg_cong)
+  also have "(g ^ totient (p ^ (k - 1))) ^ p = g ^ (p * totient (p ^ (k - 1)))"
+    by (simp add: power_mult [symmetric] mult.commute)
+  also have "p * totient (p ^ (k - 1)) = totient (p ^ k)"
+    using p \<open>k \<ge> 2\<close> by (simp add: totient_prime_power Suc_diff_Suc flip: power_Suc)
+  also have "(p ^ (k - 1) * t + 1) ^ p = (\<Sum>i\<le>p. (p choose i) * t ^ i * p ^ (i * (k - 1)))"
+    by (subst binomial) (simp_all add: mult_ac power_mult_distrib power_mult [symmetric])
+  finally have "[g ^ totient (p ^ k) = (\<Sum>i\<le>p. (p choose i) * t ^ i * p ^ (i * (k - 1)))]
+                  (mod (p ^ Suc k))" (is "[_ = ?rhs] (mod _)") by simp
+
+  also have "[?rhs = (\<Sum>i\<le>p. if i \<le> 1 then (p choose i) * t ^ i * p ^ (i * (k - 1)) else 0)]
+               (mod (p ^ Suc k))" (is "[sum ?f _ = sum ?g _] (mod _)")
+  proof (intro cong_sum)
+    fix i assume i: "i \<in> {..p}"
+    consider "i \<le> 1" | "i = 2" | "i > 2" by force
+    thus "[?f i = ?g i] (mod (p ^ Suc k))"
+    proof cases
+      assume i: "i > 2"
+      have "Suc k \<le> 3 * (k - 1)"
+        using \<open>k \<ge> 2\<close> by (simp add: algebra_simps)
+      also have "3 * (k - 1) \<le> i * (k - 1)"
+        using i by (intro mult_right_mono) auto
+      finally have "p ^ Suc k dvd ?f i"
+        by (intro dvd_mult le_imp_power_dvd)
+      thus "[?f i = ?g i] (mod (p ^ Suc k))"
+    next
+      assume [simp]: "i = 2"
+      have "?f i = p * (p - 1) div 2 * t\<^sup>2 * p ^ (2 * (k - 1))"
+        using choose_two[of p] by simp
+      also have "p * (p - 1) div 2 = (p - 1) div 2 * p"
+        using \<open>odd p\<close> by (auto elim!: oddE)
+      also have "\<dots> * t\<^sup>2 * p ^ (2 * (k - 1)) = (p - 1) div 2 * t\<^sup>2 * (p * p ^ (2 * (k - 1)))"
+      also have "p * p ^ (2 * (k - 1)) = p ^ (2 * k - 1)"
+        using \<open>k \<ge> 2\<close> by (cases k) auto
+      also have "p ^ Suc k dvd (p - 1) div 2 * t\<^sup>2 * p ^ (2 * k - 1)"
+        using \<open>k \<ge> 2\<close> by (intro dvd_mult le_imp_power_dvd) auto
+      finally show "[?f i = ?g i] (mod (p ^ Suc k))"
+    qed auto
+  qed
+  also have "(\<Sum>i\<le>p. ?g i) = (\<Sum>i\<le>1. ?f i)"
+    using p prime_gt_1_nat[of p] by (intro sum.mono_neutral_cong_right) auto
+  also have "\<dots> = 1 + t * p ^ k"
+    using choose_two[of p] \<open>k \<ge> 2\<close> by (cases k) simp_all
+  finally have eq: "[g ^ totient (p ^ k) = 1 + t * p ^ k] (mod p ^ Suc k)" .
+
+  have "[g ^ totient (p ^ k) \<noteq> 1] (mod p ^ Suc k)"
+  proof
+    assume "[g ^ totient (p ^ k) = 1] (mod p ^ Suc k)"
+    hence "[g ^ totient (p ^ k) - g ^ totient (p ^ k) = 1 + t * p ^ k - 1] (mod p ^ Suc k)"
+      by (intro cong_diff_nat eq) auto
+    hence "[t * p ^ k = 0] (mod p ^ Suc k)"
+    hence "p * p ^ k dvd t * p ^ k"
+    hence "p dvd t" using \<open>p > 2\<close> by simp
+    with \<open>\<not>p dvd t\<close> show False by contradiction
+  qed
+  thus ?case by simp
+qed
+
+text \<open>
+  We can now show that primitive roots modulo \<open>p\<close> with the above condition are
+  indeed also primitive roots modulo $p^k$.
+\<close>
+proposition residue_primroot_prime_lift_iff:
+  assumes p: "prime p" "odd p" and "residue_primroot p g"
+  shows   "(\<forall>k>0. residue_primroot (p ^ k) g) \<longleftrightarrow> [g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
+proof -
+  from assms have g: "coprime p g" "ord p g = p - 1"
+    by (auto simp: residue_primroot_def totient_prime)
+  show ?thesis
+  proof
+    assume "\<forall>k>0. residue_primroot (p ^ k) g"
+    hence "residue_primroot (p\<^sup>2) g" by auto
+    hence "ord (p\<^sup>2) g = totient (p\<^sup>2)"
+    thus "[g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
+      using g assms prime_gt_1_nat[of p]
+      by (auto simp: ord_divides' totient_prime_power)
+  next
+    assume g': "[g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
+
+    have "residue_primroot (p ^ k) g" if "k > 0" for k
+    proof (cases "k = 1")
+      case False
+      with that have k: "k > 1" by simp
+      from g have coprime: "coprime (p ^ k) g"
+        by (auto simp: totatives_def coprime_commute)
+
+      define t where "t = ord (p ^ k) g"
+      have "[g ^ t = 1] (mod (p ^ k))"
+        by (simp add: t_def ord_divides')
+      also have "p ^ k = p * p ^ (k - 1)"
+        using k by (cases k) auto
+      finally have "[g ^ t = 1] (mod p)"
+        by (rule cong_modulus_mult_nat)
+      hence "totient p dvd t"
+        using g p by (simp add: ord_divides' totient_prime)
+      then obtain q where t: "t = totient p * q" by auto
+
+      have "t dvd totient (p ^ k)"
+        using coprime by (simp add: t_def order_divides_totient)
+      with t p k have "q dvd p ^ (k - 1)" using prime_gt_1_nat[of p]
+        by (auto simp: totient_prime totient_prime_power)
+      then obtain b where b: "b \<le> k - 1" "q = p ^ b"
+        using divides_primepow_nat[of p q "k - 1"] p by auto
+
+      have "b = k - 1"
+      proof (rule ccontr)
+        assume "b \<noteq> k - 1"
+        with b have "b < k - 1" by simp
+        have "t = p ^ b * (p - 1)"
+          using b p by (simp add: t totient_prime)
+        also have "\<dots> dvd p ^ (k - 2) * (p - 1)"
+          using \<open>b < k - 1\<close> by (intro mult_dvd_mono le_imp_power_dvd) auto
+        also have "\<dots> = totient (p ^ (k - 1))"
+          using k p by (simp add: totient_prime_power numeral_2_eq_2)
+        finally have "[g ^ totient (p ^ (k - 1)) = 1] (mod (p ^ k))"
+          by (simp add: ord_divides' t_def)
+        with residue_primroot_power_prime_power_neq_1[of k p g] p k assms g' show False
+          by auto
+      qed
+      hence "t = totient (p ^ k)"
+        using p k by (simp add: t b totient_prime totient_prime_power)
+      thus "residue_primroot (p ^ k) g"
+        using g one_less_power[of p k] prime_gt_1_nat[of p] p k
+        by (simp add: residue_primroot_def t_def)
+    qed (use assms in auto)
+    thus "\<forall>k>0. residue_primroot (p ^ k) g" by blast
+  qed
+qed
+
+text \<open>
+  If \<open>p\<close> is an odd prime, there is always a primitive root \<open>g\<close> modulo \<open>p\<close>, and if \<open>g\<close> does not
+  fulfil the above assumption required for it to be liftable to $p^k$, we can use $g + p$, which
+  is also a primitive root modulo \<open>p\<close> and \<^emph>\<open>does\<close> fulfil the assumption.
+
+  This shows that any modulus that is a power of an odd prime has a primitive root.
+\<close>
+theorem residue_primroot_odd_prime_power_exists:
+  assumes p: "prime p" "odd p"
+  obtains g where "\<forall>k>0. residue_primroot (p ^ k) g"
+proof -
+  obtain g where g: "residue_primroot p g"
+    using prime_primitive_root_exists[of p] assms prime_gt_1_nat[of p] by auto
+
+  have "\<exists>g. residue_primroot p g \<and> [g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
+  proof (cases "[g ^ (p - 1) = 1] (mod p\<^sup>2)")
+    case True
+    define g' where "g' = p + g"
+    note g
+    also have "residue_primroot p g \<longleftrightarrow> residue_primroot p g'"
+      unfolding g'_def by (rule residue_primroot_cong) (auto simp: cong_def)
+    finally have g': "residue_primroot p g'" .
+
+    have "[g' ^ (p - 1) = (\<Sum>k\<le>p-1. ((p-1) choose k) * g ^ (p - Suc k) * p ^ k)] (mod p\<^sup>2)"
+      (is "[_ = ?rhs] (mod _)") by (simp add: g'_def binomial mult_ac)
+    also have "[?rhs = (\<Sum>k\<le>p-1. if k \<le> 1 then ((p-1) choose k) *
+                                   g ^ (p - Suc k) * p ^ k else 0)] (mod p\<^sup>2)"
+      (is "[sum ?f _ = sum ?g _] (mod _)")
+    proof (intro cong_sum)
+      fix k assume "k \<in> {..p-1}"
+      show "[?f k = ?g k] (mod p\<^sup>2)"
+      proof (cases "k \<le> 1")
+        case False
+        have "p\<^sup>2 dvd ?f k"
+          using False by (intro dvd_mult le_imp_power_dvd) auto
+        thus ?thesis using False by (simp add: cong_0_iff)
+      qed auto
+    qed
+    also have "sum ?g {..p-1} = sum ?f {0, 1}"
+      using prime_gt_1_nat[of p] p by (intro sum.mono_neutral_cong_right) auto
+    also have "\<dots> = g ^ (p - 1) + p * (p - 1) * g ^ (p - 2)"
+      using p by (simp add: numeral_2_eq_2)
+    also have "[g ^ (p - 1) + p * (p - 1) * g ^ (p - 2) = 1 + p * (p - 1) * g ^ (p - 2)] (mod p\<^sup>2)"
+      by (intro cong_add True) auto
+    finally have "[g' ^ (p - 1) = 1 + p * (p - 1) * g ^ (p - 2)] (mod p\<^sup>2)" .
+
+    moreover have "[1 + p * (p - 1) * g ^ (p - 2) \<noteq> 1] (mod p\<^sup>2)"
+    proof
+      assume "[1 + p * (p - 1) * g ^ (p - 2) = 1] (mod p\<^sup>2)"
+      hence "[1 + p * (p - 1) * g ^ (p - 2) - 1 = 1 - 1] (mod p\<^sup>2)"
+        by (intro cong_diff_nat) auto
+      hence "p * p dvd p * ((p - 1) * g ^ (p - 2))"
+        by (auto simp: cong_0_iff power2_eq_square)
+      hence "p dvd (p - 1) * g ^ (p - 2)"
+        using p by simp
+      hence "p dvd g ^ (p - 2)"
+        using p dvd_imp_le[of p "p - Suc 0"] prime_gt_1_nat[of p]
+        by (auto simp: prime_dvd_mult_iff)
+      also have "\<dots> dvd g ^ (p - 1)"
+        by (intro le_imp_power_dvd) auto
+      finally have "[g ^ (p - 1) = 0] (mod p)"
+      hence "[0 = g ^ (p - 1)] (mod p)"
+
+      also from \<open>residue_primroot p g\<close> have "[g ^ (p - 1) = 1] (mod p)"
+        using p by (auto simp: residue_primroot_def ord_divides' totient_prime)
+      finally have "[0 = 1] (mod p)" .
+      thus False using prime_gt_1_nat[of p] p by (simp add: cong_def)
+    qed
+
+    ultimately have "[g' ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
+    thus "\<exists>g. residue_primroot p g \<and> [g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
+      using g' by blast
+  qed (use g in auto)
+  thus ?thesis
+    using residue_primroot_prime_lift_iff[OF assms] that by blast
+qed
+
+
+subsection \<open>Carmichael's function\<close>
+
+text \<open>
+  Carmichael's function $\lambda(n)$ gives the LCM of the orders of all elements in the
+  residue ring modulo $n$ -- or, equivalently, the maximum order, as we will show later.
+  Algebraically speaking, it is the exponent of the multiplicative group
+  $(\mathbb{Z}/n\mathbb{Z})^*$.
+
+  It is not to be confused with Liouville's function, which is also denoted by $\lambda(n)$.
+\<close>
+definition Carmichael where
+  "Carmichael n = (LCM a \<in> totatives n. ord n a)"
+
+lemma Carmichael_0 [simp]: "Carmichael 0 = 1"
+
+lemma Carmichael_1 [simp]: "Carmichael 1 = 1"
+
+lemma Carmichael_Suc_0 [simp]: "Carmichael (Suc 0) = 1"
+
+lemma ord_dvd_Carmichael:
+  assumes "n > 1" "coprime n k"
+  shows   "ord n k dvd Carmichael n"
+proof -
+  have "k mod n \<in> totatives n"
+    using assms by (auto simp: totatives_def coprime_commute intro!: Nat.gr0I)
+  hence "ord n (k mod n) dvd Carmichael n"
+    by (simp add: Carmichael_def del: ord_mod)
+  thus ?thesis by simp
+qed
+
+lemma Carmichael_divides:
+  assumes "Carmichael n dvd k" "coprime n a"
+  shows   "[a ^ k = 1] (mod n)"
+proof (cases "n < 2 \<or> a = 1")
+  case False
+  hence "ord n a dvd Carmichael n"
+    using False assms by (intro ord_dvd_Carmichael) auto
+  also have "\<dots> dvd k" by fact
+  finally have "ord n a dvd k" .
+  thus ?thesis using ord_divides by auto
+next
+  case True
+  then consider "a = 1" | "n = 0" | "n = 1" by force
+  thus ?thesis using assms by cases auto
+qed
+
+lemma Carmichael_dvd_totient: "Carmichael n dvd totient n"
+  unfolding Carmichael_def
+proof (intro Lcm_least, safe)
+  fix a assume "a \<in> totatives n"
+  hence "[a ^ totient n = 1] (mod n)"
+    by (intro euler_theorem) (auto simp: totatives_def)
+  thus "ord n a dvd totient n"
+    using ord_divides by blast
+qed
+
+lemma Carmichael_dvd_mono_coprime:
+  assumes "coprime m n" "m > 1" "n > 1"
+  shows   "Carmichael m dvd Carmichael (m * n)"
+  unfolding Carmichael_def[of m]
+proof (intro Lcm_least, safe)
+  fix x assume x: "x \<in> totatives m"
+  from assms have "totatives n \<noteq> {}" by simp
+  then obtain y where y: "y \<in> totatives n" by blast
+
+  from binary_chinese_remainder_nat[OF assms(1), of x y]
+  obtain z where z: "[z = x] (mod m)" "[z = y] (mod n)" by blast
+  have z': "coprime z n" "coprime z m"
+    by (rule cong_imp_coprime; use x y z in \<open>force simp: totatives_def cong_sym_eq\<close>)+
+
+  from z have "ord m x = ord m z"
+    by (intro ord_cong) (auto simp: cong_sym_eq)
+  also have "ord m z dvd ord (m * n) z"
+    using assms by (auto simp: ord_modulus_mult_coprime)
+  also from z' assms have "\<dots> dvd Carmichael (m * n)"
+    by (intro ord_dvd_Carmichael) (auto simp: coprime_commute intro!:one_less_mult)
+  finally show "ord m x dvd Carmichael (m * n)" .
+qed
+
+text \<open>
+  $\lambda$ distributes over the product of coprime numbers similarly to $\varphi$, but
+  with LCM instead of multiplication:
+\<close>
+lemma Carmichael_mult_coprime:
+  assumes "coprime m n"
+  shows   "Carmichael (m * n) = lcm (Carmichael m) (Carmichael n)"
+proof (cases "m \<le> 1 \<or> n \<le> 1")
+  case True
+  hence "m = 0 \<or> n = 0 \<or> m = 1 \<or> n = 1" by force
+  thus ?thesis using assms by auto
+next
+  case False
+  show ?thesis
+  proof (rule dvd_antisym)
+    show "Carmichael (m * n) dvd lcm (Carmichael m) (Carmichael n)"
+      unfolding Carmichael_def[of "m * n"]
+    proof (intro Lcm_least, safe)
+      fix x assume x: "x \<in> totatives (m * n)"
+      have "ord (m * n) x = lcm (ord m x) (ord n x)"
+        using assms x by (subst ord_modulus_mult_coprime) (auto simp: coprime_commute totatives_def)
+      also have "\<dots> dvd lcm (Carmichael m) (Carmichael n)"
+        using False x
+        by (intro lcm_mono ord_dvd_Carmichael) (auto simp: totatives_def coprime_commute)
+      finally show "ord (m * n) x dvd \<dots>" .
+    qed
+  next
+    show "lcm (Carmichael m) (Carmichael n) dvd Carmichael (m * n)"
+      using Carmichael_dvd_mono_coprime[of m n]
+            Carmichael_dvd_mono_coprime[of n m] assms False
+      by (auto intro!: lcm_least simp: coprime_commute mult.commute)
+  qed
+qed
+
+lemma Carmichael_pos [simp, intro]: "Carmichael n > 0"
+  by (auto simp: Carmichael_def ord_eq_0 totatives_def coprime_commute intro!: Nat.gr0I)
+
+lemma Carmichael_nonzero [simp]: "Carmichael n \<noteq> 0"
+  by simp
+
+lemma power_Carmichael_eq_1:
+  assumes "n > 1" "coprime n x"
+  shows   "[x ^ Carmichael n = 1] (mod n)"
+  using ord_dvd_Carmichael[of n x] assms
+  by (auto simp: ord_divides')
+
+lemma Carmichael_2 [simp]: "Carmichael 2 = 1"
+  using Carmichael_dvd_totient[of 2] by simp
+
+lemma Carmichael_4 [simp]: "Carmichael 4 = 2"
+proof -
+  have "Carmichael 4 dvd 2"
+    using Carmichael_dvd_totient[of 4] by simp
+  hence "Carmichael 4 \<le> 2" by (rule dvd_imp_le) auto
+  moreover have "Carmichael 4 \<noteq> 1"
+    using power_Carmichael_eq_1[of "4::nat" 3]
+    unfolding coprime_iff_gcd_eq_1 by (auto simp: gcd_non_0_nat cong_def)
+  ultimately show ?thesis
+    using Carmichael_pos[of 4] by linarith
+qed
+
+lemma residue_primroot_Carmichael:
+  assumes "residue_primroot n g"
+  shows   "Carmichael n = totient n"
+proof (cases "n = 1")
+  case False
+  show ?thesis
+  proof (intro dvd_antisym Carmichael_dvd_totient)
+    have "ord n g dvd Carmichael n"
+      using assms False by (intro ord_dvd_Carmichael) (auto simp: residue_primroot_def)
+    thus "totient n dvd Carmichael n"
+      using assms by (auto simp: residue_primroot_def)
+  qed
+qed auto
+
+lemma Carmichael_odd_prime_power:
+  assumes "prime p" "odd p" "k > 0"
+  shows   "Carmichael (p ^ k) = p ^ (k - 1) * (p - 1)"
+proof -
+  from assms obtain g where "residue_primroot (p ^ k) g"
+    using residue_primroot_odd_prime_power_exists[of p] assms by metis
+  hence "Carmichael (p ^ k) = totient (p ^ k)"
+    by (intro residue_primroot_Carmichael[of "p ^ k" g]) auto
+  with assms show ?thesis by (simp add: totient_prime_power)
+qed
+
+lemma Carmichael_prime:
+  assumes "prime p"
+  shows   "Carmichael p = p - 1"
+proof (cases "even p")
+  case True
+  with assms have "p = 2"
+    using primes_dvd_imp_eq two_is_prime_nat by blast
+  thus ?thesis by simp
+next
+  case False
+  with Carmichael_odd_prime_power[of p 1] assms show ?thesis by simp
+qed
+
+lemma Carmichael_twopow_ge_8:
+  assumes "k \<ge> 3"
+  shows   "Carmichael (2 ^ k) = 2 ^ (k - 2)"
+proof (intro dvd_antisym)
+  have "2 ^ (k - 2) = ord (2 ^ k) (3 :: nat)"
+    using ord_twopow_3_5[of k 3] assms by simp
+  also have "\<dots> dvd Carmichael (2 ^ k)"
+    using assms one_less_power[of "2::nat" k] by (intro ord_dvd_Carmichael) auto
+  finally show "2 ^ (k - 2) dvd \<dots>" .
+next
+  show "Carmichael (2 ^ k) dvd 2 ^ (k - 2)"
+    unfolding Carmichael_def
+  proof (intro Lcm_least, safe)
+    fix x assume "x \<in> totatives (2 ^ k)"
+    hence "odd x" by (auto simp: totatives_def)
+    hence "[x ^ 2 ^ (k - 2) = 1] (mod 2 ^ k)"
+      using assms ord_twopow_aux[of k x] by auto
+    thus "ord (2 ^ k) x dvd 2 ^ (k - 2)"
+  qed
+qed
+
+lemma Carmichael_twopow:
+  "Carmichael (2 ^ k) = (if k \<le> 2 then 2 ^ (k - 1) else 2 ^ (k - 2))"
+proof -
+  have "k = 0 \<or> k = 1 \<or> k = 2 \<or> k \<ge> 3" by linarith
+  thus ?thesis by (auto simp: Carmichael_twopow_ge_8)
+qed
+
+lemma Carmichael_prime_power:
+  assumes "prime p" "k > 0"
+  shows   "Carmichael (p ^ k) =
+             (if p = 2 \<and> k > 2 then 2 ^ (k - 2) else p ^ (k - 1) * (p - 1))"
+proof (cases "p = 2")
+  case True
+  thus ?thesis by (simp add: Carmichael_twopow)
+next
+  case False
+  with assms have "odd p" "p > 2"
+    using prime_odd_nat[of p] prime_gt_1_nat[of p] by auto
+  thus ?thesis
+    using assms Carmichael_odd_prime_power[of p k] by simp
+qed
+
+lemma Carmichael_prod_coprime:
+  assumes "finite A" "\<And>i j. i \<in> A \<Longrightarrow> j \<in> A \<Longrightarrow> i \<noteq> j \<Longrightarrow> coprime (f i) (f j)"
+  shows   "Carmichael (\<Prod>i\<in>A. f i) = (LCM i\<in>A. Carmichael (f i))"
+  using assms by (induction A rule: finite_induct)
+                 (simp, simp, subst Carmichael_mult_coprime[OF prod_coprime_right], auto)
+
+text \<open>
+  Since $\lambda$ distributes over coprime factors and we know the value of $\lambda(p^k)$
+  for prime $p$, we can now give a closed formula for $\lambda(n)$ in terms of the prime
+  factorisation of $n$:
+\<close>
+theorem Carmichael_closed_formula:
+  "Carmichael n =
+     (LCM p\<in>prime_factors n. let k = multiplicity p n
+                             in  if p = 2 \<and> k > 2 then 2 ^ (k - 2) else p ^ (k - 1) * (p - 1))"
+  (is "_ = Lcm ?A")
+proof (cases "n = 0")
+  case False
+  hence "n = (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n)"
+    using prime_factorization_nat by blast
+  also have "Carmichael \<dots> =
+               (LCM p\<in>prime_factors n. Carmichael (p ^ multiplicity p n))"
+    by (subst Carmichael_prod_coprime) (auto simp: in_prime_factors_iff primes_coprime)
+  also have "(\<lambda>p. Carmichael (p ^ multiplicity p n))  prime_factors n = ?A"
+    by (intro image_cong)
+       (auto simp: Let_def Carmichael_prime_power prime_factors_multiplicity)
+  finally show ?thesis .
+qed auto
+
+corollary even_Carmichael:
+  assumes "n > 2"
+  shows   "even (Carmichael n)"
+proof (cases "\<exists>k. n = 2 ^ k")
+  case True
+  then obtain k where [simp]: "n = 2 ^ k" by auto
+  from assms have "k \<noteq> 0" "k \<noteq> 1" by (auto intro!: Nat.gr0I)
+  hence "k \<ge> 2" by auto
+  thus ?thesis by (auto simp: Carmichael_twopow)
+next
+  case False
+  from assms have "n \<noteq> 0" by auto
+  from False have "\<exists>p\<in>prime_factors n. p \<noteq> 2"
+    using assms Ex_other_prime_factor[of n 2] by auto
+  from divide_out_primepow_ex[OF \<open>n \<noteq> 0\<close> this] guess p k n' . note p = this
+  from p have coprime: "coprime (p ^ k) n'"
+    using p prime_imp_coprime by auto
+  have "odd p"
+    using p primes_dvd_imp_eq[of 2 p] by auto
+  have "even (Carmichael (p ^ k))"
+    using p \<open>odd p\<close> by (auto simp: Carmichael_prime_power)
+  with p coprime show ?thesis
+    by (auto simp: Carmichael_mult_coprime intro!: dvd_lcmI1)
+qed
+
+lemma eval_Carmichael:
+  assumes "prime_factorization n = A"
+  shows     "Carmichael n = (LCM p \<in> set_mset A.
+               let k = count A p in if p = 2 \<and> k > 2 then 2 ^ (k - 2) else p ^ (k - 1) * (p - 1))"
+  unfolding assms [symmetric] Carmichael_closed_formula
+  by (intro arg_cong[where f = Lcm] image_cong) (auto simp: Let_def count_prime_factorization)
+
+text \<open>
+  Any residue ring always contains a $\lambda$-root, i.\,e.\ an element whose
+  order is $\lambda(n)$.
+\<close>
+theorem Carmichael_root_exists:
+  assumes "n > (0::nat)"
+  obtains g where "g \<in> totatives n" and "ord n g = Carmichael n"
+proof (cases "n = 1")
+  case True
+  thus ?thesis by (intro that[of 1]) (auto simp: totatives_def)
+next
+  case False
+  have primepow: "\<exists>g. coprime (p ^ k) g \<and> ord (p ^ k) g = Carmichael (p ^ k)"
+    if pk: "prime p" "k > 0" for p k
+  proof (cases "p = 2")
+    case [simp]: True
+    from \<open>k > 0\<close> consider "k = 1" | "k = 2" | "k \<ge> 3" by force
+    thus ?thesis
+    proof cases
+      assume "k = 1"
+      thus ?thesis by (intro exI[of _ 1]) auto
+    next
+      assume [simp]: "k = 2"
+      have "coprime 4 (3::nat)"
+        by (auto simp: coprime_iff_gcd_eq_1 gcd_non_0_nat)
+      thus ?thesis by (intro exI[of _ 3]) auto
+    next
+      assume k: "k \<ge> 3"
+      have "coprime (2 ^ k :: nat) 3" by auto
+      thus ?thesis using k
+        by (intro exI[of _ 3]) (auto simp: ord_twopow_3_5 Carmichael_twopow)
+    qed
+  next
+    case False
+    hence "odd p" using \<open>prime p\<close>
+      using primes_dvd_imp_eq two_is_prime_nat by blast
+    then obtain g where "residue_primroot (p ^ k) g"
+      using residue_primroot_odd_prime_power_exists[of p] pk by metis
+    thus ?thesis using False pk
+      by (intro exI[of _ g])
+         (auto simp: Carmichael_prime_power residue_primroot_def totient_prime_power)
+  qed
+
+  define P where "P = prime_factors n"
+  define k where "k = (\<lambda>p. multiplicity p n)"
+  have "\<forall>p\<in>P. \<exists>g. coprime (p ^ k p) g \<and> ord (p ^ k p) g = Carmichael (p ^ k p)"
+    using primepow by (auto simp: P_def k_def prime_factors_multiplicity)
+  hence "\<exists>g. \<forall>p\<in>P. coprime (p ^ k p) (g p) \<and> ord (p ^ k p) (g p) = Carmichael (p ^ k p)"
+    by (subst (asm) bchoice_iff)
+  then obtain g where g: "\<And>p. p \<in> P \<Longrightarrow> coprime (p ^ k p) (g p)"
+                         "\<And>p. p \<in> P \<Longrightarrow> ord (p ^ k p) (g p) = Carmichael (p ^ k p)" by metis
+  have "\<exists>x. \<forall>i\<in>P. [x = g i] (mod i ^ k i)"
+    by (intro chinese_remainder_nat)
+       (auto simp: P_def k_def in_prime_factors_iff primes_coprime)
+  then obtain x where x: "\<And>p. p \<in> P \<Longrightarrow> [x = g p] (mod p ^ k p)" by metis
+
+  have "n = (\<Prod>p\<in>P. p ^ k p)"
+    using assms unfolding P_def k_def by (rule prime_factorization_nat)
+  also have "ord \<dots> x = (LCM p\<in>P. ord (p ^ k p) x)"
+    by (intro ord_modulus_prod_coprime) (auto simp: P_def in_prime_factors_iff primes_coprime)
+  also have "(\<lambda>p. ord (p ^ k p) x)  P = (\<lambda>p. ord (p ^ k p) (g p))  P"
+    by (intro image_cong ord_cong x) auto
+  also have "\<dots> = (\<lambda>p. Carmichael (p ^ k p))  P"
+    by (intro image_cong g) auto
+  also have "Lcm \<dots> = Carmichael (\<Prod>p\<in>P. p ^ k p)"
+    by (intro Carmichael_prod_coprime [symmetric])
+       (auto simp: P_def in_prime_factors_iff primes_coprime)
+  also have "(\<Prod>p\<in>P. p ^ k p) = n"
+    using assms unfolding P_def k_def by (rule prime_factorization_nat [symmetric])
+  finally have "ord n x = Carmichael n" .
+  moreover from this have "coprime n x"
+    by (cases "coprime n x") (auto split: if_splits)
+  ultimately show ?thesis using assms False
+    by (intro that[of "x mod n"])
+       (auto simp: totatives_def coprime_commute coprime_absorb_left intro!: Nat.gr0I)
+qed
+
+text \<open>
+  This also means that the Carmichael number is not only the LCM of the orders
+  of the elements of the residue ring, but indeed the maximum of the orders.
+\<close>
+lemma Carmichael_altdef:
+  "Carmichael n = (if n = 0 then 1 else Max (ord n  totatives n))"
+proof (cases "n = 0")
+  case False
+  have "Carmichael n = Max (ord n  totatives n)"
+  proof (intro antisym Max.boundedI Max.coboundedI)
+    fix k assume k: "k \<in> ord n  totatives n"
+    thus "k \<le> Carmichael n"
+    proof (cases "n = 1")
+      case False
+      with \<open>n \<noteq> 0\<close> have "n > 1" by linarith
+      thus ?thesis using k \<open>n \<noteq> 0\<close>
+        by (intro dvd_imp_le)
+           (auto intro!: ord_dvd_Carmichael simp: totatives_def coprime_commute)
+    qed auto
+  next
+    obtain g where "g \<in> totatives n" and "ord n g = Carmichael n"
+      using Carmichael_root_exists[of n] \<open>n \<noteq> 0\<close> by auto
+    thus "Carmichael n \<in> ord n  totatives n" by force
+  qed (use \<open>n \<noteq> 0\<close> in auto)
+  thus ?thesis using False by simp
+qed auto
+
+
+subsection \<open>Existence of primitive roots for general moduli\<close>
+
+text \<open>
+  We now related Carmichael's function to the existence of primitive roots and, in the end,
+  use this to show precisely which moduli have primitive roots and which do not.
+
+  The first criterion for the existence of a primitive root is this: A primitive root modulo $n$
+  exists iff $\lambda(n) = \varphi(n)$.
+\<close>
+lemma Carmichael_eq_totient_imp_primroot:
+  assumes "n > 0" and "Carmichael n = totient n"
+  shows   "\<exists>g. residue_primroot n g"
+proof -
+  from \<open>n > 0\<close> obtain g where "g \<in> totatives n" and "ord n g = Carmichael n"
+    using Carmichael_root_exists[of n] by metis
+  with assms show ?thesis by (auto simp: residue_primroot_def totatives_def coprime_commute)
+qed
+
+theorem residue_primroot_iff_Carmichael:
+  "(\<exists>g. residue_primroot n g) \<longleftrightarrow> Carmichael n = totient n \<and> n > 0"
+proof safe
+  fix g assume g: "residue_primroot n g"
+  thus "n > 0" by (auto simp: residue_primroot_def)
+  have "coprime n g" by (rule ccontr) (use g in \<open>auto simp: residue_primroot_def\<close>)
+
+  show "Carmichael n = totient n"
+  proof (cases "n = 1")
+    case False
+    with \<open>n > 0\<close> have "n > 1" by auto
+    with \<open>coprime n g\<close> have "ord n g dvd Carmichael n"
+      by (intro ord_dvd_Carmichael) auto
+    thus ?thesis using g by (intro dvd_antisym Carmichael_dvd_totient)
+                            (auto simp: residue_primroot_def)
+  qed auto
+qed (use Carmichael_eq_totient_imp_primroot[of n] in auto)
+
+text \<open>
+  Any primitive root modulo $mn$ for coprime $m$, $n$ is also a primitive root modulo $m$ and $n$.
+  The converse does not hold in general.
+\<close>
+lemma residue_primroot_modulus_mult_coprimeD:
+  assumes "coprime m n" and "residue_primroot (m * n) g"
+  shows   "residue_primroot m g" "residue_primroot n g"
+proof -
+  have *: "m > 0" "n > 0" "coprime m g" "coprime n g"
+          "lcm (ord m g) (ord n g) = totient m * totient n"
+    using assms
+    by (auto simp: residue_primroot_def ord_modulus_mult_coprime totient_mult_coprime)
+
+  define a b where "a = totient m div ord m g" and "b = totient n div ord n g"
+  have ab: "totient m = ord m g * a" "totient n = ord n g * b"
+    using * by (auto simp: a_def b_def order_divides_totient)
+
+  have "a = 1" "b = 1" "coprime (ord m g) (ord n g)"
+    unfolding coprime_iff_gcd_eq_1 using * by (auto simp: ab lcm_nat_def dvd_div_eq_mult ord_eq_0)
+  with ab and * show "residue_primroot m g" "residue_primroot n g"
+    by (auto simp: residue_primroot_def)
+qed
+
+text \<open>
+  If a primitive root modulo $mn$ exists for coprime $m, n$, then $\lambda(m)$ and $\lambda(n)$
+  must also be coprime. This is helpful in establishing that there are no primitive roots
+  modulo $mn$ by showing e.\,g.\ that $\lambda(m)$ and $\lambda(n)$ are both even.
+\<close>
+lemma residue_primroot_modulus_mult_coprime_imp_Carmichael_coprime:
+  assumes "coprime m n" and "residue_primroot (m * n) g"
+  shows   "coprime (Carmichael m) (Carmichael n)"
+proof -
+  from residue_primroot_modulus_mult_coprimeD[OF assms]
+    have *: "residue_primroot m g" "residue_primroot n g" by auto
+  hence [simp]: "Carmichael m = totient m" "Carmichael n = totient n"
+  from * have mn: "m > 0" "n > 0" by (auto simp: residue_primroot_def)
+
+  from assms have "Carmichael (m * n) = totient (m * n) \<and> n > 0"
+    using residue_primroot_iff_Carmichael[of "m * n"] by auto
+  with assms have "lcm (totient m) (totient n) = totient m * totient n"
+    by (simp add: Carmichael_mult_coprime totient_mult_coprime)
+  thus ?thesis unfolding coprime_iff_gcd_eq_1 using mn
+    by (simp add: lcm_nat_def dvd_div_eq_mult)
+qed
+
+text \<open>
+  The following moduli are precisely those that have primitive roots.
+\<close>
+definition cyclic_moduli :: "nat set" where
+  "cyclic_moduli = {1, 2, 4} \<union> {p ^ k |p k. prime p \<and> odd p \<and> k > 0} \<union>
+                     {2 * p ^ k |p k. prime p \<and> odd p \<and> k > 0}"
+
+theorem residue_primroot_iff_in_cyclic_moduli:
+  "(\<exists>g. residue_primroot m g) \<longleftrightarrow> m \<in> cyclic_moduli"
+proof -
+  have "(\<exists>g. residue_primroot m g)" if "m \<in> cyclic_moduli"
+  using that unfolding cyclic_moduli_def
+  by (intro Carmichael_eq_totient_imp_primroot)
+     (auto dest: prime_gt_0_nat simp: Carmichael_prime_power totient_prime_power
+                 Carmichael_mult_coprime totient_mult_coprime)
+
+  moreover have "\<not>(\<exists>g. residue_primroot m g)" if "m \<notin> cyclic_moduli"
+  proof (cases "m = 0")
+    case False
+    with that have [simp]: "m > 0" "m \<noteq> 1" by (auto simp: cyclic_moduli_def)
+    show ?thesis
+    proof (cases "\<exists>k. m = 2 ^ k")
+      case True
+      then obtain k where [simp]: "m = 2 ^ k" by auto
+      with that have "k \<noteq> 0 \<and> k \<noteq> 1 \<and> k \<noteq> 2" by (auto simp: cyclic_moduli_def)
+      hence "k \<ge> 3" by auto
+      thus ?thesis by (subst residue_primroot_iff_Carmichael)
+                      (auto simp: Carmichael_twopow totient_prime_power)
+    next
+      case False
+      hence "\<exists>p\<in>prime_factors m. p \<noteq> 2"
+        using Ex_other_prime_factor[of m 2] by auto
+      from divide_out_primepow_ex[OF \<open>m \<noteq> 0\<close> this]
+      obtain p k m' where p: "p \<noteq> 2" "prime p" "p dvd m" "\<not>p dvd m'" "0 < k" "m = p ^ k * m'"
+        by metis
+      have "odd p"
+        using p primes_dvd_imp_eq[of 2 p] by auto
+      from p have coprime: "coprime (p ^ k) m'"
+        using p prime_imp_coprime by auto
+      have "m \<in> cyclic_moduli" if "m' = 1"
+        using that p \<open>odd p\<close> by (auto simp: cyclic_moduli_def)
+      moreover have "m \<in> cyclic_moduli" if "m' = 2"
+      proof -
+        have "m = 2 * p ^ k" using p that by (simp add: mult.commute)
+        thus "m \<in> cyclic_moduli" using p \<open>odd p\<close>
+          unfolding cyclic_moduli_def by blast
+      qed
+      moreover have "m' \<noteq> 0" using p by (intro notI) auto
+      ultimately have "m' \<noteq> 0 \<and>m' \<noteq> 1 \<and> m' \<noteq> 2" using that by auto
+      hence "m' > 2" by linarith
+
+      show ?thesis
+      proof
+        assume "\<exists>g. residue_primroot m g"
+        with coprime p have coprime': "coprime (p - 1) (Carmichael m')"
+          using residue_primroot_modulus_mult_coprime_imp_Carmichael_coprime[OF coprime]
+          by (auto simp: Carmichael_prime_power)
+        moreover have "even (p - 1)" "even (Carmichael m')"
+          using \<open>m' > 2\<close> \<open>odd p\<close> by (auto intro!: even_Carmichael)
+        ultimately show False by force
+      qed
+    qed
+  qed auto
+
+  ultimately show ?thesis by metis
+qed
+
+lemma residue_primroot_is_generator:
+  assumes "m > 1" and "residue_primroot m g"
+  shows   "bij_betw (\<lambda>i. g ^ i mod m) {..<totient m} (totatives m)"
+  unfolding bij_betw_def
+proof
+  from assms have [simp]: "ord m g = totient m"
+  from assms have "coprime m g" by (simp add: residue_primroot_def)
+  hence "inj_on (\<lambda>i. g ^ i mod m) {..<ord m g}"
+    by (intro inj_power_mod)
+  thus inj: "inj_on (\<lambda>i. g ^ i mod m) {..<totient m}"
+    by simp
+
+  show "(\<lambda>i. g ^ i mod m)  {..<totient m} = totatives m"
+  proof (rule card_subset_eq)
+    show "card ((\<lambda>i. g ^ i mod m)  {..<totient m}) = card (totatives m)"
+      using inj by (subst card_image) (auto simp: totient_def)
+    show "(\<lambda>i. g ^ i mod m)  {..<totient m} \<subseteq> totatives m"
+      using \<open>m > 1\<close> \<open>coprime m g\<close> power_in_totatives[of m g] by blast
+  qed auto
+qed
+
+text \<open>
+  Given one primitive root \<open>g\<close>, all the primitive roots are powers $g^i$ for
+  $1\leq i \leq \varphi(n)$ with $\text{gcd}(i, \varphi(n)) = 1$.
+\<close>
+theorem residue_primroot_bij_betw_primroots:
+  assumes "m > 1" and "residue_primroot m g"
+  shows   "bij_betw (\<lambda>i. g ^ i mod m) (totatives (totient m))
+                                      {g\<in>totatives m. residue_primroot m g}"
+proof (cases "m = 2")
+  case [simp]: True
+  have [simp]: "totatives 2 = {1}"
+    by (auto simp: totatives_def elim!: oddE)
+  from assms have "odd g"
+    by (auto simp: residue_primroot_def)
+  hence pow_eq: "(\<lambda>i. g ^ i mod m) = (\<lambda>_. 1)"
+    by (auto simp: fun_eq_iff mod_2_eq_odd)
+  have "{g \<in> totatives m. residue_primroot m g} = {1}"
+    by (auto simp: residue_primroot_def)
+  thus ?thesis using pow_eq by (auto simp: bij_betw_def)
+next
+  case False
+  thus ?thesis unfolding bij_betw_def
+  proof safe
+    from assms False have "m > 2" by auto
+    from assms \<open>m > 2\<close> have "totient m > 1" by (intro totient_gt_1) auto
+    from assms have [simp]: "ord m g = totient m"
+    from assms have "coprime m g" by (simp add: residue_primroot_def)
+    hence "inj_on (\<lambda>i. g ^ i mod m) {..<ord m g}"
+      by (intro inj_power_mod)
+    thus "inj_on (\<lambda>i. g ^ i mod m) (totatives (totient m))"
+      by (rule inj_on_subset)
+         (use assms \<open>totient m > 1\<close> in \<open>auto simp: totatives_less residue_primroot_def\<close>)
+
+    {
+      fix i assume i: "i \<in> totatives (totient m)"
+      from \<open>coprime m g\<close> and \<open>m > 2\<close> show "g ^ i mod m \<in> totatives m"
+        by (intro power_in_totatives) auto
+      show "residue_primroot m (g ^ i mod m)"
+        using i \<open>m > 2\<close> \<open>coprime m g\<close>
+        by (auto simp: residue_primroot_def coprime_commute ord_power totatives_def)
+    }
+    {
+      fix x assume x: "x \<in> totatives m" "residue_primroot m x"
+      then obtain i where i: "i < totient m" "x = (g ^ i mod m)"
+        using assms residue_primroot_is_generator[of m g] by (auto simp: bij_betw_def)
+      from i x \<open>m > 2\<close> have "i > 0" by (intro Nat.gr0I) (auto simp: residue_primroot_1_iff)
+      have "totient m div gcd i (totient m) = totient m"
+        using x i \<open>coprime m g\<close> by (auto simp add: residue_primroot_def ord_power)
+      hence "coprime i (totient m)"
+        unfolding coprime_iff_gcd_eq_1 using assms by (subst (asm) dvd_div_eq_mult) auto
+      with i \<open>i > 0\<close> have "i \<in> totatives (totient m)" by (auto simp: totatives_def)
+      thus "x \<in> (\<lambda>i. g ^ i mod m)  totatives (totient m)" using i by auto
+    }
+  qed
+qed
+
+text \<open>
+  It follows from the above statement that any residue ring modulo \<open>n\<close> that \<^emph>\<open>has\<close> primitive roots
+  has exactly $\varphi(\varphi(n))$ of them.
+\<close>
+corollary card_residue_primroots:
+  assumes "\<exists>g. residue_primroot m g"
+  shows   "card {g\<in>totatives m. residue_primroot m g} = totient (totient m)"
+proof (cases "m = 1")
+  case [simp]: True
+  have "{g \<in> totatives m. residue_primroot m g} = {1}"
+    by (auto simp: residue_primroot_def)
+  thus ?thesis by simp
+next
+  case False
+  from assms obtain g where g: "residue_primroot m g" by auto
+  hence "m \<noteq> 0" by (intro notI) auto
+  with \<open>m \<noteq> 1\<close> have "m > 1" by linarith
+  from this g have "bij_betw (\<lambda>i. g ^ i mod m) (totatives (totient m))
+                      {g\<in>totatives m. residue_primroot m g}"
+    by (rule residue_primroot_bij_betw_primroots)
+  hence "card (totatives (totient m)) = card {g\<in>totatives m. residue_primroot m g}"
+    by (rule bij_betw_same_card)
+  thus ?thesis by (simp add: totient_def)
+qed
+
+corollary card_residue_primroots':
+  "card {g\<in>totatives m. residue_primroot m g} =
+     (if m \<in> cyclic_moduli then totient (totient m) else 0)"
+  by (simp add: residue_primroot_iff_in_cyclic_moduli [symmetric] card_residue_primroots)
+
+text \<open>
+  As an example, we evaluate $\lambda(122200)$ using the prime factorisation.
+\<close>
+lemma "Carmichael 122200 = 1380"
+proof -
+  have "prime_factorization (2^3 * 5^2 * 13 * 47) = {#2, 2, 2, 5, 5, 13, 47::nat#}"
+    by (intro prime_factorization_eqI) auto
+  from eval_Carmichael[OF this] show "Carmichael 122200 = 1380"
+    by (simp add: lcm_nat_def gcd_non_0_nat)
+qed
+
+(* TODO: definition of index ("discrete logarithm") *)
+
+end
\ No newline at end of file
--- a/src/HOL/Number_Theory/Residues.thy	Sat Feb 02 15:52:14 2019 +0100
+++ b/src/HOL/Number_Theory/Residues.thy	Mon Feb 04 12:16:03 2019 +0100
@@ -398,7 +398,7 @@
shows "a \<ge> 0 \<Longrightarrow> p \<ge> 0 \<Longrightarrow> (nat a ^ n) mod (nat p) = nat ((a ^ n) mod p)"
by (simp add: int_one_le_iff_zero_less nat_mod_distrib order_less_imp_le nat_power_eq[symmetric])

-theorem residue_prime_mult_group_has_gen :
+theorem residue_prime_mult_group_has_gen:
fixes p :: nat
assumes prime_p : "prime p"
shows "\<exists>a \<in> {1 .. p - 1}. {1 .. p - 1} = {a^i mod p|i . i \<in> UNIV}"
@@ -455,4 +455,52 @@
ultimately show ?thesis ..
qed

+
+subsection \<open>Upper bound for the number of $n$-th roots\<close>
+
+lemma roots_mod_prime_bound:
+  fixes n c p :: nat
+  assumes "prime p" "n > 0"
+  defines "A \<equiv> {x\<in>{..<p}. [x ^ n = c] (mod p)}"
+  shows   "card A \<le> n"
+proof -
+  define R where "R = residue_ring (int p)"
+  term monom
+  from assms(1) interpret residues_prime p R
+    by unfold_locales (simp_all add: R_def)
+  interpret R: UP_domain R "UP R" by (unfold_locales)
+
+  let ?f = "UnivPoly.monom (UP R) \<one>\<^bsub>R\<^esub> n \<ominus>\<^bsub>(UP R)\<^esub> UnivPoly.monom (UP R) (int (c mod p)) 0"
+  have in_carrier: "int (c mod p) \<in> carrier R"
+    using prime_gt_1_nat[OF assms(1)] by (simp add: R_def residue_ring_def)
+
+  have "deg R ?f = n"
+    using assms in_carrier by (simp add: R.deg_minus_eq)
+  hence f_not_zero: "?f \<noteq> \<zero>\<^bsub>UP R\<^esub>" using assms by (auto simp add : R.deg_nzero_nzero)
+  have roots_bound: "finite {a \<in> carrier R. UnivPoly.eval R R id a ?f = \<zero>\<^bsub>R\<^esub>} \<and>
+                     card {a \<in> carrier R. UnivPoly.eval R R id a ?f = \<zero>\<^bsub>R\<^esub>} \<le> deg R ?f"
+                    using finite in_carrier by (intro R.roots_bound[OF _ f_not_zero]) simp
+  have subs: "{x \<in> carrier R. x [^]\<^bsub>R\<^esub> n = int (c mod p)} \<subseteq>
+                {a \<in> carrier R. UnivPoly.eval R R id a ?f = \<zero>\<^bsub>R\<^esub>}"
+    using in_carrier by (auto simp: R.evalRR_simps)
+  then have "card {x \<in> carrier R. x [^]\<^bsub>R\<^esub> n = int (c mod p)} \<le>
+               card {a \<in> carrier R. UnivPoly.eval R R id a ?f = \<zero>\<^bsub>R\<^esub>}"
+    using finite by (intro card_mono) auto
+  also have "\<dots> \<le> n"
+    using \<open>deg R ?f = n\<close> roots_bound by linarith
+  also {
+    fix x assume "x \<in> carrier R"
+    hence "x [^]\<^bsub>R\<^esub> n = (x ^ n) mod (int p)"
+      by (subst pow_cong [symmetric]) (auto simp: R_def residue_ring_def)
+  }
+  hence "{x \<in> carrier R. x [^]\<^bsub>R\<^esub> n = int (c mod p)} = {x \<in> carrier R. [x ^ n = int c] (mod p)}"
+    by (fastforce simp: cong_def zmod_int)
+  also have "bij_betw int A {x \<in> carrier R. [x ^ n = int c] (mod p)}"
+    by (rule bij_betwI[of int _ _ nat])
+       (use cong_int_iff in \<open>force simp: R_def residue_ring_def A_def\<close>)+
+  from bij_betw_same_card[OF this] have "card {x \<in> carrier R. [x ^ n = int c] (mod p)} = card A" ..
+  finally show ?thesis .
+qed
+
+
end
--- a/src/HOL/Number_Theory/Totient.thy	Sat Feb 02 15:52:14 2019 +0100
+++ b/src/HOL/Number_Theory/Totient.thy	Mon Feb 04 12:16:03 2019 +0100
@@ -62,6 +62,21 @@
shows "n - 1 \<in> totatives n"
using assms coprime_diff_one_left_nat [of n] by (simp add: in_totatives_iff)

+lemma power_in_totatives:
+  assumes "m > 1" "coprime m g"
+  shows   "g ^ i mod m \<in> totatives m"
+proof -
+  have "\<not>m dvd g ^ i"
+  proof
+    assume "m dvd g ^ i"
+    hence "\<not>coprime m (g ^ i)"
+      using \<open>m > 1\<close> by (subst coprime_absorb_left) auto
+    with \<open>coprime m g\<close> show False by simp
+  qed
+  with assms show ?thesis
+    by (auto simp: totatives_def coprime_commute intro!: Nat.gr0I)
+qed
+
lemma totatives_prime_power_Suc:
assumes "prime p"
shows   "totatives (p ^ Suc n) = {0<..p^Suc n} - (\<lambda>m. p * m)  {0<..p^n}"
@@ -198,6 +213,18 @@
lemma totient_gt_0_iff [simp]: "totient n > 0 \<longleftrightarrow> n > 0"
by (auto intro: Nat.gr0I)

+lemma totient_gt_1:
+  assumes "n > 2"
+  shows   "totient n > 1"
+proof -
+  have "{1, n - 1} \<subseteq> totatives n"
+    using assms coprime_diff_one_left_nat[of n] by (auto simp: totatives_def)
+  hence "card {1, n - 1} \<le> card (totatives n)"
+    by (intro card_mono) auto
+  thus ?thesis using assms
+qed
+
lemma card_gcd_eq_totient:
"n > 0 \<Longrightarrow> d dvd n \<Longrightarrow> card {k\<in>{0<..n}. gcd k n = d} = totient (n div d)"
unfolding totient_def by (rule sym, rule bij_betw_same_card[OF bij_betw_totatives_gcd_eq])
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Number_Theory/document/root.bib	Mon Feb 04 12:16:03 2019 +0100
@@ -0,0 +1,10 @@
+@book{apostol1976analytic,
+	series = "Undergraduate {T}exts in {M}athematics",
+	title = "Introduction to {A}nalytic {N}umber {T}heory",
+	year = 1976,
+	author = "Tom M. Apostol",
+	publisher = "Springer-Verlag",
+	doi = "10.1007/978-1-4757-5579-4",
+	isbn = "978-0-387-90163-3"
+}
+
--- a/src/HOL/Number_Theory/document/root.tex	Sat Feb 02 15:52:14 2019 +0100
+++ b/src/HOL/Number_Theory/document/root.tex	Mon Feb 04 12:16:03 2019 +0100
@@ -26,5 +26,8 @@

\input{session}

+\bibliographystyle{abbrv}
+\bibliography{root}
+
\end{document}