--- 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 @@
by (simp_all add: div mod)
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
+ Quadratic_Reciprocity
+ 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"
+ by (simp add: ord_def)
+
+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)"
+ by (simp add: ord_divides')
+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
+ by (simp add: ord_divides')
+ 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))"
+ by (simp add: power_mult)
+ finally have "ord m a dvd k * ord m (a ^ k)"
+ by (simp add: ord_divides')
+ 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)"
+ by (simp add: power_add)
+ 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)"
+ by (simp add: cong_sym_eq)
+ 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"
+ by (simp add: ord_divides')
+ 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"
+ by (metis \<open>0 < x\<close> add.commute add_diff_inverse_nat less_one neq0_conv power_eq_0_iff)
+ 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]
+ power_even_eq[symmetric] power_add [symmetric])
+ also have "[\<dots> = 0 + 0 + 1] (mod 2 ^ Suc k)"
+ using \<open>2 * k \<ge> Suc k\<close>
+ by (intro cong_add)
+ (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'))"
+ by (simp_all add: ord_divides')
+ 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)"
+ by (simp add: ord_divides')
+ 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')"
+ by (subst power2_eq_square) (simp add: algebra_simps flip: power_add)
+ 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')"
+ by (subst power2_eq_square) (simp add: algebra_simps flip: power_add)
+ 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)"
+ by (simp add: cong_sym_eq)
+ hence "2 ^ k dvd 2 ^ (k - 1)"
+ by (simp add: cong_0_iff)
+ 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)"
+ by (simp add: ord_divides')
+ 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)"
+ by (simp add: ord_divides')
+ 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)"
+ by (simp add: cong_def)
+ 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"
+ by (simp add: residue_primroot.simps)
+
+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)"
+ by (simp add: totient_def)
+ 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))"
+ by (simp add: cong_0_iff)
+ 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)))"
+ by (simp add: algebra_simps)
+ 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))"
+ by (simp add: cong_0_iff)
+ 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)"
+ by (simp add: cong_sym_eq)
+ hence "p * p ^ k dvd t * p ^ k"
+ by (simp add: cong_0_iff)
+ 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)"
+ by (simp_all add: residue_primroot_def)
+ 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)"
+ by (simp add: cong_0_iff)
+ hence "[0 = g ^ (p - 1)] (mod p)"
+ by (simp add: cong_sym_eq)
+
+ 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)"
+ by (simp add: cong_def)
+ 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"
+ by (simp add: Carmichael_def)
+
+lemma Carmichael_1 [simp]: "Carmichael 1 = 1"
+ by (simp add: Carmichael_def)
+
+lemma Carmichael_Suc_0 [simp]: "Carmichael (Suc 0) = 1"
+ by (simp add: Carmichael_def)
+
+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)"
+ by (simp add: ord_divides')
+ 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"
+ by (simp_all add: residue_primroot_Carmichael)
+ 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"
+ by (simp add: residue_primroot_def)
+ 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"
+ by (simp add: residue_primroot_def)
+ 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
+ by (simp add: totient_def)
+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}