(* File: HOL/Number_Theory/Residue_Primitive_Roots.thy Author: Manuel Eberl Primitive roots in residue rings: Definition and existence criteria *) section ‹Primitive roots in residue rings and Carmichael's function› theory Residue_Primitive_Roots imports Pocklington begin text ‹ 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 › subsection ‹Primitive roots in residue rings› text ‹ A primitive root of a residue ring modulo ‹n› is an element ‹g› that ∗‹generates› the ring, i.\,e.\ such that for each ‹x› coprime to ‹n› there exists an ‹i› such that $x = g^i$. A simpler definition is that ‹g› must have the same order as the cardinality of the multiplicative group, which is $\varphi(n)$. Note that for convenience, this definition does ∗‹not› demand ‹g < n›. › inductive residue_primroot :: "nat ⇒ nat ⇒ bool" where "n > 0 ⟹ coprime n g ⟹ ord n g = totient n ⟹ residue_primroot n g" lemma residue_primroot_def [code]: "residue_primroot n x ⟷ n > 0 ∧ coprime n x ∧ 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 ⟷ n = 1" by (auto simp: residue_primroot_def) lemma residue_primroot_1_iff: "residue_primroot n (Suc 0) ⟷ n ∈ {1, 2}" proof assume *: "residue_primroot n (Suc 0)" with totient_gt_1[of n] have "n ≤ 2" by (cases "n ≤ 2") (auto simp: residue_primroot_def) hence "n ∈ {0, 1, 2}" by auto thus "n ∈ {1, 2}" using * by (auto simp: residue_primroot_def) qed (auto simp: residue_primroot_def) subsection ‹Primitive roots modulo a prime› text ‹ For prime ‹p›, we now analyse the number of elements in the ring $\mathbb{Z}/p\mathbb{Z}$ whose order is precisely ‹d› for each ‹d›. › context fixes n :: nat and ψ assumes n: "n > 1" defines "ψ ≡ (λd. card {x∈totatives n. ord n x = d})" begin lemma elements_with_ord_restrict_totatives: "d > 0 ⟹ {x∈{..<n}. ord n x = d} = {x∈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 "ψ d ≠ 0" and "prime n" and a: "a ∈ totatives n" "ord n a = d" "a ≠ 1" shows "inj_on (λk. a ^ k mod n) {..<d}" and "{x∈{..<n}. [x ^ d = 1] (mod n)} = (λk. a ^ k mod n) ` {..<d}" and "bij_betw (λk. a ^ k mod n) (totatives d) {x∈{..<n}. ord n x = d}" proof - show inj: "inj_on (λ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 ≠ 1" using a n by (auto simp: ord_eq_Suc_0_iff totatives_less cong_def) ultimately have d: "d > 1" by simp have *: "(λk. a ^ k mod n) ` {..<d} = {x∈{..<n}. [x ^ d = 1] (mod n)}" proof (rule card_seteq) have "card {x∈{..<n}. [x ^ d = 1] (mod n)} ≤ d" using assms a by (intro roots_mod_prime_bound) (auto simp: totatives_def coprime_commute) also have "… = card ((λk. a ^ k mod n) ` {..<d})" using inj by (subst card_image) auto finally show "card {x ∈ {..<n}. [x ^ d = 1] (mod n)} ≤ …" . next show "(λk. a ^ k mod n) ` {..<d} ⊆ {x ∈ {..<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 ‹auto simp: ord_divides'›) thus "[(a ^ k mod n) ^ d = 1] (mod n)" by (simp add: power_mult [symmetric] cong_def power_mod mult.commute) qed (use ‹prime n› in ‹auto dest: prime_gt_1_nat›) qed auto thus "{x∈{..<n}. [x ^ d = 1] (mod n)} = (λk. a ^ k mod n) ` {..<d}" .. show "bij_betw (λk. a ^ k mod n) (totatives d) {x∈{..<n}. ord n x = d}" unfolding bij_betw_def proof (intro conjI inj_on_subset[OF inj] equalityI subsetI) fix b assume "b ∈ (λk. a ^ k mod n) ` totatives d" then obtain k where "b = a ^ k mod n" "k ∈ totatives d" by auto thus "b ∈ {b ∈ {..<n}. ord n b = d}" using n a by (simp add: ord_power totatives_def coprime_commute) next fix b assume "b ∈ {x ∈ {..<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 ∈ {x∈{..<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 ‹coprime n b› 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 ∈ totatives d" by (auto simp: totatives_def intro!: Nat.gr0I) with k show "b ∈ (λk. a ^ k mod n) ` totatives d" by blast qed (use d n in ‹auto simp: totatives_less›) qed lemma prime_card_elements_with_ord: assumes "ψ d ≠ 0" and "prime n" shows "ψ d = totient d" proof (cases "d = 1") case True have "ψ 1 = 1" using elements_with_ord_1[of n] n by (simp add: ψ_def) thus ?thesis using True by simp next case False from assms obtain a where a: "a ∈ totatives n" "ord n a = d" by (auto simp: ψ_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 ≠ 1" by auto from bij_betw_same_card[OF prime_elements_with_ord(3)[OF assms a this]] show "ψ d = totient d" using elements_with_ord_restrict_totatives[of d] False a ‹d > 0› by (simp add: ψ_def totient_def) qed lemma prime_sum_card_elements_with_ord_eq_totient: "(∑d | d dvd totient n. ψ d) = totient n" proof - have "totient n = card (totatives n)" by (simp add: totient_def) also have "totatives n = (⋃d∈{d. d dvd totient n}. {x∈totatives n. ord n x = d})" by (force simp: order_divides_totient totatives_def coprime_commute) also have "card … = (∑d | d dvd totient n. ψ d)" unfolding ψ_def using n by (subst card_UN_disjoint) (auto intro!: finite_divisors_nat) finally show ?thesis .. qed text ‹ We can now show that the number of elements of order ‹d› is $\varphi(d)$ if $d\mid p - 1$ and 0 otherwise. › theorem prime_card_elements_with_ord_eq_totient: assumes "prime n" shows "ψ 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: ψ_def totient_prime totatives_def coprime_commute[of n]) next case True have "ψ d = totient d" proof (rule ccontr) assume neq: "ψ d ≠ totient d" have le: "ψ d ≤ totient d" if "d dvd totient n" for d using prime_card_elements_with_ord[of d] assms by (cases "ψ d = 0") auto from neq and le[of d] and True have less: "ψ d < totient d" by auto have "totient n = (∑d | d dvd totient n. ψ d)" using prime_sum_card_elements_with_ord_eq_totient .. also have "… < (∑d | d dvd totient n. totient d)" by (rule sum_strict_mono_ex1) (use n le less assms True in ‹auto intro!: finite_divisors_nat›) also have "… = 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 ‹ As a corollary, we get that the number of primitive roots modulo a prime ‹p› is $\varphi(p - 1)$. Since this number is positive, we also get that there ∗‹is› at least one primitive root modulo ‹p›. › lemma assumes "prime n" shows prime_card_primitive_roots: "card {x∈totatives n. ord n x = n - 1} = totient (n - 1)" "card {x∈{..<n}. ord n x = n - 1} = totient (n - 1)" and prime_primitive_root_exists: "∃x. residue_primroot n x" proof - show *: "card {x∈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 ψ_def) thus "card {x∈{..<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 "∃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 ‹Primitive roots modulo powers of an odd prime› text ‹ Any primitive root ‹g› modulo an odd prime ‹p› 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. › lemma residue_primroot_power_prime_power_neq_1: assumes "k ≥ 2" assumes p: "prime p" "odd p" and "residue_primroot p g" and "[g ^ (p - 1) ≠ 1] (mod p⇧^{2})" shows "[g ^ totient (p ^ (k - 1)) ≠ 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 "¬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 ‹k ≥ 2› 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 ‹k ≥ 2› by (simp add: totient_prime_power Suc_diff_Suc flip: power_Suc) also have "(p ^ (k - 1) * t + 1) ^ p = (∑i≤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) = (∑i≤p. (p choose i) * t ^ i * p ^ (i * (k - 1)))] (mod (p ^ Suc k))" (is "[_ = ?rhs] (mod _)") by simp also have "[?rhs = (∑i≤p. if i ≤ 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 ∈ {..p}" consider "i ≤ 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 ≤ 3 * (k - 1)" using ‹k ≥ 2› by (simp add: algebra_simps) also have "3 * (k - 1) ≤ 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⇧^{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 ‹odd p› by (auto elim!: oddE) also have "… * t⇧^{2}* p ^ (2 * (k - 1)) = (p - 1) div 2 * t⇧^{2}* (p * p ^ (2 * (k - 1)))" by (simp add: algebra_simps) also have "p * p ^ (2 * (k - 1)) = p ^ (2 * k - 1)" using ‹k ≥ 2› by (cases k) auto also have "p ^ Suc k dvd (p - 1) div 2 * t⇧^{2}* p ^ (2 * k - 1)" using ‹k ≥ 2› 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 "(∑i≤p. ?g i) = (∑i≤1. ?f i)" using p prime_gt_1_nat[of p] by (intro sum.mono_neutral_cong_right) auto also have "… = 1 + t * p ^ k" using choose_two[of p] ‹k ≥ 2› 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) ≠ 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 ‹p > 2› by simp with ‹¬p dvd t› show False by contradiction qed thus ?case by simp qed text ‹ We can now show that primitive roots modulo ‹p› with the above condition are indeed also primitive roots modulo $p^k$. › proposition residue_primroot_prime_lift_iff: assumes p: "prime p" "odd p" and "residue_primroot p g" shows "(∀k>0. residue_primroot (p ^ k) g) ⟷ [g ^ (p - 1) ≠ 1] (mod p⇧^{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 "∀k>0. residue_primroot (p ^ k) g" hence "residue_primroot (p⇧^{2}) g" by auto hence "ord (p⇧^{2}) g = totient (p⇧^{2})" by (simp_all add: residue_primroot_def) thus "[g ^ (p - 1) ≠ 1] (mod p⇧^{2})" using g assms prime_gt_1_nat[of p] by (auto simp: ord_divides' totient_prime_power) next assume g': "[g ^ (p - 1) ≠ 1] (mod p⇧^{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 ≤ 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 ≠ 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 "… dvd p ^ (k - 2) * (p - 1)" using ‹b < k - 1› by (intro mult_dvd_mono le_imp_power_dvd) auto also have "… = 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 "∀k>0. residue_primroot (p ^ k) g" by blast qed qed text ‹ If ‹p› is an odd prime, there is always a primitive root ‹g› modulo ‹p›, and if ‹g› 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 ‹p› and ∗‹does› fulfil the assumption. This shows that any modulus that is a power of an odd prime has a primitive root. › theorem residue_primroot_odd_prime_power_exists: assumes p: "prime p" "odd p" obtains g where "∀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 "∃g. residue_primroot p g ∧ [g ^ (p - 1) ≠ 1] (mod p⇧^{2})" proof (cases "[g ^ (p - 1) = 1] (mod p⇧^{2})") case True define g' where "g' = p + g" note g also have "residue_primroot p g ⟷ 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) = (∑k≤p-1. ((p-1) choose k) * g ^ (p - Suc k) * p ^ k)] (mod p⇧^{2})" (is "[_ = ?rhs] (mod _)") by (simp add: g'_def binomial mult_ac) also have "[?rhs = (∑k≤p-1. if k ≤ 1 then ((p-1) choose k) * g ^ (p - Suc k) * p ^ k else 0)] (mod p⇧^{2})" (is "[sum ?f _ = sum ?g _] (mod _)") proof (intro cong_sum) fix k assume "k ∈ {..p-1}" show "[?f k = ?g k] (mod p⇧^{2})" proof (cases "k ≤ 1") case False have "p⇧^{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 "… = 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⇧^{2})" by (intro cong_add True) auto finally have "[g' ^ (p - 1) = 1 + p * (p - 1) * g ^ (p - 2)] (mod p⇧^{2})" . moreover have "[1 + p * (p - 1) * g ^ (p - 2) ≠ 1] (mod p⇧^{2})" proof assume "[1 + p * (p - 1) * g ^ (p - 2) = 1] (mod p⇧^{2})" hence "[1 + p * (p - 1) * g ^ (p - 2) - 1 = 1 - 1] (mod p⇧^{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 "… 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 ‹residue_primroot p g› 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) ≠ 1] (mod p⇧^{2})" by (simp add: cong_def) thus "∃g. residue_primroot p g ∧ [g ^ (p - 1) ≠ 1] (mod p⇧^{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 ‹Carmichael's function› text ‹ 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)$. › definition Carmichael where "Carmichael n = (LCM a ∈ 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 ∈ 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 ∨ a = 1") case False hence "ord n a dvd Carmichael n" using False assms by (intro ord_dvd_Carmichael) auto also have "… 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 ∈ 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 ∈ totatives m" from assms have "totatives n ≠ {}" by simp then obtain y where y: "y ∈ 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 ‹force simp: totatives_def cong_sym_eq›)+ 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 "… 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 ‹ $\lambda$ distributes over the product of coprime numbers similarly to $\varphi$, but with LCM instead of multiplication: › lemma Carmichael_mult_coprime: assumes "coprime m n" shows "Carmichael (m * n) = lcm (Carmichael m) (Carmichael n)" proof (cases "m ≤ 1 ∨ n ≤ 1") case True hence "m = 0 ∨ n = 0 ∨ m = 1 ∨ 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 ∈ 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 "… 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 …" . 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 ≠ 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 ≤ 2" by (rule dvd_imp_le) auto moreover have "Carmichael 4 ≠ 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 ≥ 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 "… 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 …" . next show "Carmichael (2 ^ k) dvd 2 ^ (k - 2)" unfolding Carmichael_def proof (intro Lcm_least, safe) fix x assume "x ∈ 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 ≤ 2 then 2 ^ (k - 1) else 2 ^ (k - 2))" proof - have "k = 0 ∨ k = 1 ∨ k = 2 ∨ k ≥ 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 ∧ 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" "⋀i j. i ∈ A ⟹ j ∈ A ⟹ i ≠ j ⟹ coprime (f i) (f j)" shows "Carmichael (∏i∈A. f i) = (LCM i∈A. Carmichael (f i))" using assms by (induction A rule: finite_induct) (simp, simp, subst Carmichael_mult_coprime[OF prod_coprime_right], auto) text ‹ 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$: › theorem Carmichael_closed_formula: "Carmichael n = (LCM p∈prime_factors n. let k = multiplicity p n in if p = 2 ∧ k > 2 then 2 ^ (k - 2) else p ^ (k - 1) * (p - 1))" (is "_ = Lcm ?A") proof (cases "n = 0") case False hence "n = (∏p∈prime_factors n. p ^ multiplicity p n)" using prime_factorization_nat by blast also have "Carmichael … = (LCM p∈prime_factors n. Carmichael (p ^ multiplicity p n))" by (subst Carmichael_prod_coprime) (auto simp: in_prime_factors_iff primes_coprime) also have "(λ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 "∃k. n = 2 ^ k") case True then obtain k where [simp]: "n = 2 ^ k" by auto from assms have "k ≠ 0" "k ≠ 1" by (auto intro!: Nat.gr0I) hence "k ≥ 2" by auto thus ?thesis by (auto simp: Carmichael_twopow) next case False from assms have "n ≠ 0" by auto from False have "∃p∈prime_factors n. p ≠ 2" using assms Ex_other_prime_factor[of n 2] by auto from divide_out_primepow_ex[OF ‹n ≠ 0› this] obtain p k n' where p: "p ≠ 2" "prime p" "p dvd n" "¬ p dvd n'" "0 < k" "n = p ^ k * n'" . 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 ‹odd p› 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 ∈ set_mset A. let k = count A p in if p = 2 ∧ 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 ‹ Any residue ring always contains a $\lambda$-root, i.\,e.\ an element whose order is $\lambda(n)$. › theorem Carmichael_root_exists: assumes "n > (0::nat)" obtains g where "g ∈ 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: "∃g. coprime (p ^ k) g ∧ ord (p ^ k) g = Carmichael (p ^ k)" if pk: "prime p" "k > 0" for p k proof (cases "p = 2") case [simp]: True from ‹k > 0› consider "k = 1" | "k = 2" | "k ≥ 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 ≥ 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 ‹prime p› 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 = (λp. multiplicity p n)" have "∀p∈P. ∃g. coprime (p ^ k p) g ∧ ord (p ^ k p) g = Carmichael (p ^ k p)" using primepow by (auto simp: P_def k_def prime_factors_multiplicity) hence "∃g. ∀p∈P. coprime (p ^ k p) (g p) ∧ ord (p ^ k p) (g p) = Carmichael (p ^ k p)" by (subst (asm) bchoice_iff) then obtain g where g: "⋀p. p ∈ P ⟹ coprime (p ^ k p) (g p)" "⋀p. p ∈ P ⟹ ord (p ^ k p) (g p) = Carmichael (p ^ k p)" by metis have "∃x. ∀i∈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: "⋀p. p ∈ P ⟹ [x = g p] (mod p ^ k p)" by metis have "n = (∏p∈P. p ^ k p)" using assms unfolding P_def k_def by (rule prime_factorization_nat) also have "ord … x = (LCM p∈P. ord (p ^ k p) x)" by (intro ord_modulus_prod_coprime) (auto simp: P_def in_prime_factors_iff primes_coprime) also have "(λp. ord (p ^ k p) x) ` P = (λp. ord (p ^ k p) (g p)) ` P" by (intro image_cong ord_cong x) auto also have "… = (λp. Carmichael (p ^ k p)) ` P" by (intro image_cong g) auto also have "Lcm … = Carmichael (∏p∈P. p ^ k p)" by (intro Carmichael_prod_coprime [symmetric]) (auto simp: P_def in_prime_factors_iff primes_coprime) also have "(∏p∈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 ‹ 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. › 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 ∈ ord n ` totatives n" thus "k ≤ Carmichael n" proof (cases "n = 1") case False with ‹n ≠ 0› have "n > 1" by linarith thus ?thesis using k ‹n ≠ 0› by (intro dvd_imp_le) (auto intro!: ord_dvd_Carmichael simp: totatives_def coprime_commute) qed auto next obtain g where "g ∈ totatives n" and "ord n g = Carmichael n" using Carmichael_root_exists[of n] ‹n ≠ 0› by auto thus "Carmichael n ∈ ord n ` totatives n" by force qed (use ‹n ≠ 0› in auto) thus ?thesis using False by simp qed auto subsection ‹Existence of primitive roots for general moduli› text ‹ 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)$. › lemma Carmichael_eq_totient_imp_primroot: assumes "n > 0" and "Carmichael n = totient n" shows "∃g. residue_primroot n g" proof - from ‹n > 0› obtain g where "g ∈ 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: "(∃g. residue_primroot n g) ⟷ Carmichael n = totient n ∧ 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 ‹auto simp: residue_primroot_def›) show "Carmichael n = totient n" proof (cases "n = 1") case False with ‹n > 0› have "n > 1" by auto with ‹coprime n g› 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 ‹ 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. › 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 ‹ 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. › 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) ∧ 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 ‹ The following moduli are precisely those that have primitive roots. › definition cyclic_moduli :: "nat set" where "cyclic_moduli = {1, 2, 4} ∪ {p ^ k |p k. prime p ∧ odd p ∧ k > 0} ∪ {2 * p ^ k |p k. prime p ∧ odd p ∧ k > 0}" theorem residue_primroot_iff_in_cyclic_moduli: "(∃g. residue_primroot m g) ⟷ m ∈ cyclic_moduli" proof - have "(∃g. residue_primroot m g)" if "m ∈ 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 "¬(∃g. residue_primroot m g)" if "m ∉ cyclic_moduli" proof (cases "m = 0") case False with that have [simp]: "m > 0" "m ≠ 1" by (auto simp: cyclic_moduli_def) show ?thesis proof (cases "∃k. m = 2 ^ k") case True then obtain k where [simp]: "m = 2 ^ k" by auto with that have "k ≠ 0 ∧ k ≠ 1 ∧ k ≠ 2" by (auto simp: cyclic_moduli_def) hence "k ≥ 3" by auto thus ?thesis by (subst residue_primroot_iff_Carmichael) (auto simp: Carmichael_twopow totient_prime_power) next case False hence "∃p∈prime_factors m. p ≠ 2" using Ex_other_prime_factor[of m 2] by auto from divide_out_primepow_ex[OF ‹m ≠ 0› this] obtain p k m' where p: "p ≠ 2" "prime p" "p dvd m" "¬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 ∈ cyclic_moduli" if "m' = 1" using that p ‹odd p› by (auto simp: cyclic_moduli_def) moreover have "m ∈ cyclic_moduli" if "m' = 2" proof - have "m = 2 * p ^ k" using p that by (simp add: mult.commute) thus "m ∈ cyclic_moduli" using p ‹odd p› unfolding cyclic_moduli_def by blast qed moreover have "m' ≠ 0" using p by (intro notI) auto ultimately have "m' ≠ 0 ∧m' ≠ 1 ∧ m' ≠ 2" using that by auto hence "m' > 2" by linarith show ?thesis proof assume "∃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 ‹m' > 2› ‹odd p› 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 (λ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 (λi. g ^ i mod m) {..<ord m g}" by (intro inj_power_mod) thus inj: "inj_on (λi. g ^ i mod m) {..<totient m}" by simp show "(λi. g ^ i mod m) ` {..<totient m} = totatives m" proof (rule card_subset_eq) show "card ((λi. g ^ i mod m) ` {..<totient m}) = card (totatives m)" using inj by (subst card_image) (auto simp: totient_def) show "(λi. g ^ i mod m) ` {..<totient m} ⊆ totatives m" using ‹m > 1› ‹coprime m g› power_in_totatives[of m g] by blast qed auto qed text ‹ Given one primitive root ‹g›, all the primitive roots are powers $g^i$ for $1\leq i \leq \varphi(n)$ with $\text{gcd}(i, \varphi(n)) = 1$. › theorem residue_primroot_bij_betw_primroots: assumes "m > 1" and "residue_primroot m g" shows "bij_betw (λi. g ^ i mod m) (totatives (totient m)) {g∈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: "(λi. g ^ i mod m) = (λ_. 1)" by (auto simp: fun_eq_iff mod_2_eq_odd) have "{g ∈ 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 ‹m > 2› 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 (λi. g ^ i mod m) {..<ord m g}" by (intro inj_power_mod) thus "inj_on (λi. g ^ i mod m) (totatives (totient m))" by (rule inj_on_subset) (use assms ‹totient m > 1› in ‹auto simp: totatives_less residue_primroot_def›) { fix i assume i: "i ∈ totatives (totient m)" from ‹coprime m g› and ‹m > 2› show "g ^ i mod m ∈ totatives m" by (intro power_in_totatives) auto show "residue_primroot m (g ^ i mod m)" using i ‹m > 2› ‹coprime m g› by (auto simp: residue_primroot_def coprime_commute ord_power totatives_def) } { fix x assume x: "x ∈ 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 ‹m > 2› 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 ‹coprime m g› 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 ‹i > 0› have "i ∈ totatives (totient m)" by (auto simp: totatives_def) thus "x ∈ (λi. g ^ i mod m) ` totatives (totient m)" using i by auto } qed qed text ‹ It follows from the above statement that any residue ring modulo ‹n› that ∗‹has› primitive roots has exactly $\varphi(\varphi(n))$ of them. › corollary card_residue_primroots: assumes "∃g. residue_primroot m g" shows "card {g∈totatives m. residue_primroot m g} = totient (totient m)" proof (cases "m = 1") case [simp]: True have "{g ∈ 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 ≠ 0" by (intro notI) auto with ‹m ≠ 1› have "m > 1" by linarith from this g have "bij_betw (λi. g ^ i mod m) (totatives (totient m)) {g∈totatives m. residue_primroot m g}" by (rule residue_primroot_bij_betw_primroots) hence "card (totatives (totient m)) = card {g∈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∈totatives m. residue_primroot m g} = (if m ∈ cyclic_moduli then totient (totient m) else 0)" by (simp add: residue_primroot_iff_in_cyclic_moduli [symmetric] card_residue_primroots) text ‹ As an example, we evaluate $\lambda(122200)$ using the prime factorisation. › 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