src/HOL/Number_Theory/Residue_Primitive_Roots.thy
changeset 69785 9e326f6f8a24
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Number_Theory/Residue_Primitive_Roots.thy	Mon Feb 04 12:16:03 2019 +0100
     1.3 @@ -0,0 +1,1152 @@
     1.4 +(*
     1.5 +  File:      HOL/Number_Theory/Residue_Primitive_Roots.thy
     1.6 +  Author:    Manuel Eberl
     1.7 +
     1.8 +  Primitive roots in residue rings: Definition and existence criteria
     1.9 +*)
    1.10 +section \<open>Primitive roots in residue rings and Carmichael's function\<close>
    1.11 +theory Residue_Primitive_Roots
    1.12 +  imports Pocklington
    1.13 +begin
    1.14 +
    1.15 +text \<open>
    1.16 +  This theory develops the notions of primitive roots (generators) in residue rings. It also
    1.17 +  provides a definition and all the basic properties of Carmichael's function $\lambda(n)$, which
    1.18 +  is strongly related to this. The proofs mostly follow Apostol's presentation
    1.19 +\<close>
    1.20 +
    1.21 +subsection \<open>Primitive roots in residue rings\<close>
    1.22 +
    1.23 +text \<open>
    1.24 +  A primitive root of a residue ring modulo \<open>n\<close> is an element \<open>g\<close> that \<^emph>\<open>generates\<close> the
    1.25 +  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$.
    1.26 +  A simpler definition is that \<open>g\<close> must have the same order as the cardinality of the
    1.27 +  multiplicative group, which is $\varphi(n)$.
    1.28 +
    1.29 +  Note that for convenience, this definition does \<^emph>\<open>not\<close> demand \<open>g < n\<close>.
    1.30 +\<close>
    1.31 +inductive residue_primroot :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
    1.32 +  "n > 0 \<Longrightarrow> coprime n g \<Longrightarrow> ord n g = totient n \<Longrightarrow> residue_primroot n g"
    1.33 +
    1.34 +lemma residue_primroot_def [code]:
    1.35 +  "residue_primroot n x \<longleftrightarrow> n > 0 \<and> coprime n x \<and> ord n x = totient n"
    1.36 +  by (simp add: residue_primroot.simps)
    1.37 +
    1.38 +lemma not_residue_primroot_0 [simp]: "~residue_primroot 0 x"
    1.39 +  by (auto simp: residue_primroot_def)
    1.40 +
    1.41 +lemma residue_primroot_mod [simp]: "residue_primroot n (x mod n) = residue_primroot n x"
    1.42 +  by (cases "n = 0") (simp_all add: residue_primroot_def)
    1.43 +
    1.44 +lemma residue_primroot_cong:
    1.45 +  assumes "[x = x'] (mod n)"
    1.46 +  shows   "residue_primroot n x = residue_primroot n x'"
    1.47 +proof -
    1.48 +  have "residue_primroot n x = residue_primroot n (x mod n)"
    1.49 +    by simp
    1.50 +  also have "x mod n = x' mod n"
    1.51 +    using assms by (simp add: cong_def)
    1.52 +  also have "residue_primroot n (x' mod n) = residue_primroot n x'"
    1.53 +    by simp
    1.54 +  finally show ?thesis .
    1.55 +qed
    1.56 +
    1.57 +lemma not_residue_primroot_0_right [simp]: "residue_primroot n 0 \<longleftrightarrow> n = 1"
    1.58 +  by (auto simp: residue_primroot_def)
    1.59 +
    1.60 +lemma residue_primroot_1_iff: "residue_primroot n (Suc 0) \<longleftrightarrow> n \<in> {1, 2}"
    1.61 +proof
    1.62 +  assume *: "residue_primroot n (Suc 0)"
    1.63 +  with totient_gt_1[of n] have "n \<le> 2" by (cases "n \<le> 2") (auto simp: residue_primroot_def)
    1.64 +  hence "n \<in> {0, 1, 2}" by auto
    1.65 +  thus "n \<in> {1, 2}" using * by (auto simp: residue_primroot_def)
    1.66 +qed (auto simp: residue_primroot_def)
    1.67 +
    1.68 +
    1.69 +subsection \<open>Primitive roots modulo a prime\<close>
    1.70 +
    1.71 +text \<open>
    1.72 +  For prime \<open>p\<close>, we now analyse the number of elements in the ring $\mathbb{Z}/p\mathbb{Z}$
    1.73 +  whose order is precisely \<open>d\<close> for each \<open>d\<close>.
    1.74 +\<close>
    1.75 +context
    1.76 +  fixes n :: nat and \<psi>
    1.77 +  assumes n: "n > 1"
    1.78 +  defines "\<psi> \<equiv> (\<lambda>d. card {x\<in>totatives n. ord n x = d})"
    1.79 +begin
    1.80 +
    1.81 +lemma elements_with_ord_restrict_totatives:
    1.82 +  "d > 0 \<Longrightarrow> {x\<in>{..<n}. ord n x = d} = {x\<in>totatives n. ord n x = d}"
    1.83 +  using n by (auto simp: totatives_def coprime_commute intro!: Nat.gr0I le_neq_trans)
    1.84 +
    1.85 +lemma prime_elements_with_ord:
    1.86 +  assumes "\<psi> d \<noteq> 0" and "prime n"
    1.87 +      and a: "a \<in> totatives n" "ord n a = d" "a \<noteq> 1"
    1.88 +  shows   "inj_on (\<lambda>k. a ^ k mod n) {..<d}"
    1.89 +    and   "{x\<in>{..<n}. [x ^ d = 1] (mod n)} = (\<lambda>k. a ^ k mod n) ` {..<d}"
    1.90 +    and   "bij_betw (\<lambda>k. a ^ k mod n) (totatives d) {x\<in>{..<n}. ord n x = d}"
    1.91 +proof -
    1.92 +  show inj: "inj_on (\<lambda>k. a ^ k mod n) {..<d}"
    1.93 +    using inj_power_mod[of n a] a by (auto simp: totatives_def coprime_commute)
    1.94 +  from a have "d > 0" by (auto simp: totatives_def coprime_commute)
    1.95 +  moreover have "d \<noteq> 1" using a n
    1.96 +    by (auto simp: ord_eq_Suc_0_iff totatives_less cong_def)
    1.97 +  ultimately have d: "d > 1" by simp
    1.98 +
    1.99 +  have *: "(\<lambda>k. a ^ k mod n) ` {..<d} = {x\<in>{..<n}. [x ^ d = 1] (mod n)}"
   1.100 +  proof (rule card_seteq)
   1.101 +    have "card {x\<in>{..<n}. [x ^ d = 1] (mod n)} \<le> d"
   1.102 +      using assms a by (intro roots_mod_prime_bound) (auto simp: totatives_def coprime_commute)
   1.103 +    also have "\<dots> = card ((\<lambda>k. a ^ k mod n) ` {..<d})"
   1.104 +      using inj by (subst card_image) auto
   1.105 +    finally show "card {x \<in> {..<n}. [x ^ d = 1] (mod n)} \<le> \<dots>" .
   1.106 +  next
   1.107 +    show "(\<lambda>k. a ^ k mod n) ` {..<d} \<subseteq> {x \<in> {..<n}. [x ^ d = 1] (mod n)}"
   1.108 +    proof safe
   1.109 +      fix k assume "k < d"
   1.110 +      have "[(a ^ d) ^ k = 1 ^ k] (mod n)"
   1.111 +        by (intro cong_pow) (use a in \<open>auto simp: ord_divides'\<close>)
   1.112 +      thus "[(a ^ k mod n) ^ d = 1] (mod n)"
   1.113 +        by (simp add: power_mult [symmetric] cong_def power_mod mult.commute)
   1.114 +    qed (use \<open>prime n\<close> in \<open>auto dest: prime_gt_1_nat\<close>)
   1.115 +  qed auto
   1.116 +  thus "{x\<in>{..<n}. [x ^ d = 1] (mod n)} = (\<lambda>k. a ^ k mod n) ` {..<d}" ..
   1.117 +
   1.118 +  show "bij_betw (\<lambda>k. a ^ k mod n) (totatives d) {x\<in>{..<n}. ord n x = d}"
   1.119 +    unfolding bij_betw_def
   1.120 +  proof (intro conjI inj_on_subset[OF inj] equalityI subsetI)
   1.121 +    fix b assume "b \<in> (\<lambda>k. a ^ k mod n) ` totatives d"
   1.122 +    then obtain k where "b = a ^ k mod n" "k \<in> totatives d" by auto
   1.123 +    thus "b \<in> {b \<in> {..<n}. ord n b = d}"
   1.124 +      using n a by (simp add: ord_power totatives_def coprime_commute)
   1.125 +  next
   1.126 +    fix b assume "b \<in> {x \<in> {..<n}. ord n x = d}"
   1.127 +    hence b: "ord n b = d" "b < n" by auto
   1.128 +    with d have "coprime n b" using ord_eq_0[of n b] by auto
   1.129 +    from b have "b \<in> {x\<in>{..<n}. [x ^ d = 1] (mod n)}"
   1.130 +      by (auto simp: ord_divides')
   1.131 +    with * obtain k where k: "k < d" "b = a ^ k mod n"
   1.132 +      by blast
   1.133 +    with b(2) n a d have "d div gcd k d = ord n b"
   1.134 +      using \<open>coprime n b\<close> by (auto simp: ord_power)
   1.135 +    also have "ord n b = d" by (simp add: b)
   1.136 +    finally have "coprime k d"
   1.137 +      unfolding coprime_iff_gcd_eq_1 using d a by (subst (asm) div_eq_dividend_iff) auto
   1.138 +    with k b d have "k \<in> totatives d" by (auto simp: totatives_def intro!: Nat.gr0I)
   1.139 +    with k show "b \<in> (\<lambda>k. a ^ k mod n) ` totatives d" by blast
   1.140 +  qed (use d n in \<open>auto simp: totatives_less\<close>)
   1.141 +qed
   1.142 +
   1.143 +lemma prime_card_elements_with_ord:
   1.144 +  assumes "\<psi> d \<noteq> 0" and "prime n"
   1.145 +  shows   "\<psi> d = totient d"
   1.146 +proof (cases "d = 1")
   1.147 +  case True
   1.148 +  have "\<psi> 1 = 1"
   1.149 +    using elements_with_ord_1[of n] n by (simp add: \<psi>_def)
   1.150 +  thus ?thesis using True by simp
   1.151 +next
   1.152 +  case False
   1.153 +  from assms obtain a where a: "a \<in> totatives n" "ord n a = d"
   1.154 +    by (auto simp: \<psi>_def)
   1.155 +  from a have "d > 0" by (auto intro!: Nat.gr0I simp: ord_eq_0 totatives_def coprime_commute)
   1.156 +  from a and False have "a \<noteq> 1" by auto
   1.157 +  from bij_betw_same_card[OF prime_elements_with_ord(3)[OF assms a this]] show "\<psi> d = totient d"
   1.158 +    using elements_with_ord_restrict_totatives[of d] False a \<open>d > 0\<close>
   1.159 +    by (simp add: \<psi>_def totient_def)
   1.160 +qed
   1.161 +
   1.162 +lemma prime_sum_card_elements_with_ord_eq_totient:
   1.163 +  "(\<Sum>d | d dvd totient n. \<psi> d) = totient n"
   1.164 +proof -
   1.165 +  have "totient n = card (totatives n)"
   1.166 +    by (simp add: totient_def)
   1.167 +  also have "totatives n = (\<Union>d\<in>{d. d dvd totient n}. {x\<in>totatives n. ord n x = d})"
   1.168 +    by (force simp: order_divides_totient totatives_def coprime_commute)
   1.169 +  also have "card \<dots> = (\<Sum>d | d dvd totient n. \<psi> d)"
   1.170 +    unfolding \<psi>_def using n by (subst card_UN_disjoint) (auto intro!: finite_divisors_nat)
   1.171 +  finally show ?thesis ..
   1.172 +qed
   1.173 +
   1.174 +text \<open>
   1.175 +  We can now show that the number of elements of order \<open>d\<close> is $\varphi(d)$ if $d\mid p - 1$
   1.176 +  and 0 otherwise.
   1.177 +\<close>
   1.178 +theorem prime_card_elements_with_ord_eq_totient:
   1.179 +  assumes "prime n"
   1.180 +  shows   "\<psi> d = (if d dvd n - 1 then totient d else 0)"
   1.181 +proof (cases "d dvd totient n")
   1.182 +  case False
   1.183 +  thus ?thesis using order_divides_totient[of n] assms
   1.184 +    by (auto simp: \<psi>_def totient_prime totatives_def coprime_commute[of n])
   1.185 +next
   1.186 +  case True
   1.187 +  have "\<psi> d = totient d"
   1.188 +  proof (rule ccontr)
   1.189 +    assume neq: "\<psi> d \<noteq> totient d"
   1.190 +    have le: "\<psi> d \<le> totient d" if "d dvd totient n" for d
   1.191 +      using prime_card_elements_with_ord[of d] assms by (cases "\<psi> d = 0") auto
   1.192 +    from neq and le[of d] and True have less: "\<psi> d < totient d" by auto
   1.193 +  
   1.194 +    have "totient n = (\<Sum>d | d dvd totient n. \<psi> d)"
   1.195 +      using prime_sum_card_elements_with_ord_eq_totient ..
   1.196 +    also have "\<dots> < (\<Sum>d | d dvd totient n. totient d)"
   1.197 +      by (rule sum_strict_mono_ex1)
   1.198 +         (use n le less assms True in \<open>auto intro!: finite_divisors_nat\<close>)
   1.199 +    also have "\<dots> = totient n"
   1.200 +      using totient_divisor_sum .
   1.201 +    finally show False by simp
   1.202 +  qed
   1.203 +  with True show ?thesis using assms by (simp add: totient_prime)
   1.204 +qed
   1.205 +
   1.206 +text \<open>
   1.207 +  As a corollary, we get that the number of primitive roots modulo a prime \<open>p\<close> is
   1.208 +  $\varphi(p - 1)$. Since this number is positive, we also get that there \<^emph>\<open>is\<close> at least
   1.209 +  one primitive root modulo \<open>p\<close>.
   1.210 +\<close>
   1.211 +lemma
   1.212 +  assumes "prime n"
   1.213 +  shows   prime_card_primitive_roots:  "card {x\<in>totatives n. ord n x = n - 1} = totient (n - 1)"
   1.214 +                                       "card {x\<in>{..<n}. ord n x = n - 1} = totient (n - 1)"
   1.215 +  and     prime_primitive_root_exists: "\<exists>x. residue_primroot n x"
   1.216 +proof -
   1.217 +  show *: "card {x\<in>totatives n. ord n x = n - 1} = totient (n - 1)"
   1.218 +    using prime_card_elements_with_ord_eq_totient[of "n - 1"] assms
   1.219 +    by (auto simp: totient_prime \<psi>_def)
   1.220 +  thus "card {x\<in>{..<n}. ord n x = n - 1} = totient (n - 1)"
   1.221 +    using assms n elements_with_ord_restrict_totatives[of "n - 1"] by simp
   1.222 +  
   1.223 +  note *
   1.224 +  also have "totient (n - 1) > 0" using n by auto
   1.225 +  finally show "\<exists>x. residue_primroot n x" using assms prime_gt_1_nat[of n]
   1.226 +    by (subst (asm) card_gt_0_iff)
   1.227 +       (auto simp: residue_primroot_def totient_prime totatives_def coprime_commute)
   1.228 +qed
   1.229 +
   1.230 +end
   1.231 +
   1.232 +
   1.233 +subsection \<open>Primitive roots modulo powers of an odd prime\<close>
   1.234 +
   1.235 +text \<open>
   1.236 +  Any primitive root \<open>g\<close> modulo an odd prime \<open>p\<close> is also a primitive root modulo $p^k$ for all
   1.237 +  $k > 0$ if $[g^{p - 1} \neq 1]\ (\text{mod}\ p^2)$. To show this, we first need the
   1.238 +  following lemma.
   1.239 +\<close>
   1.240 +lemma residue_primroot_power_prime_power_neq_1:
   1.241 +  assumes "k \<ge> 2"
   1.242 +  assumes p: "prime p" "odd p" and "residue_primroot p g" and "[g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
   1.243 +  shows   "[g ^ totient (p ^ (k - 1)) \<noteq> 1] (mod (p ^ k))"
   1.244 +  using assms(1)
   1.245 +proof (induction k rule: dec_induct)
   1.246 +  case base
   1.247 +  thus ?case using assms by (simp add: totient_prime)
   1.248 +next
   1.249 +  case (step k)
   1.250 +  from p have "p > 2"
   1.251 +    using prime_gt_1_nat[of p] by (cases "p = 2") auto
   1.252 +  from assms have g: "g > 0" by (auto intro!: Nat.gr0I)
   1.253 +  have "[g ^ totient (p ^ (k - 1)) = 1] (mod p ^ (k - 1))"
   1.254 +    using assms by (intro euler_theorem)
   1.255 +                   (auto simp: residue_primroot_def totatives_def coprime_commute)
   1.256 +  from cong_to_1_nat[OF this]
   1.257 +    obtain t where *: "g ^ totient (p ^ (k - 1)) - 1 = p ^ (k - 1) * t" by auto
   1.258 +  have t: "g ^ totient (p ^ (k - 1)) = p ^ (k - 1) * t + 1"
   1.259 +    using g by (subst * [symmetric]) auto 
   1.260 +
   1.261 +  have "\<not>p dvd t"
   1.262 +  proof
   1.263 +    assume "p dvd t"
   1.264 +    then obtain q where [simp]: "t = p * q" by auto
   1.265 +    from t have "g ^ totient (p ^ (k - 1)) = p ^ k * q + 1"
   1.266 +      using \<open>k \<ge> 2\<close> by (cases k) auto
   1.267 +    hence "[g ^ totient (p ^ (k - 1)) = p ^ k * q + 1] (mod p ^ k)"
   1.268 +      by simp
   1.269 +    also have "[p ^ k * q + 1 = 0 * q + 1] (mod p ^ k)"
   1.270 +      by (intro cong_add cong_mult) (auto simp: cong_0_iff)
   1.271 +    finally have "[g ^ totient (p ^ (k - 1)) = 1] (mod p ^ k)"
   1.272 +      by simp
   1.273 +    with step.IH show False by contradiction
   1.274 +  qed
   1.275 +
   1.276 +  from t have "(g ^ totient (p ^ (k - 1))) ^ p = (p ^ (k - 1) * t + 1) ^ p"
   1.277 +    by (rule arg_cong)
   1.278 +  also have "(g ^ totient (p ^ (k - 1))) ^ p = g ^ (p * totient (p ^ (k - 1)))"
   1.279 +    by (simp add: power_mult [symmetric] mult.commute)
   1.280 +  also have "p * totient (p ^ (k - 1)) = totient (p ^ k)"
   1.281 +    using p \<open>k \<ge> 2\<close> by (simp add: totient_prime_power Suc_diff_Suc flip: power_Suc)
   1.282 +  also have "(p ^ (k - 1) * t + 1) ^ p = (\<Sum>i\<le>p. (p choose i) * t ^ i * p ^ (i * (k - 1)))"
   1.283 +    by (subst binomial) (simp_all add: mult_ac power_mult_distrib power_mult [symmetric])
   1.284 +  finally have "[g ^ totient (p ^ k) = (\<Sum>i\<le>p. (p choose i) * t ^ i * p ^ (i * (k - 1)))]
   1.285 +                  (mod (p ^ Suc k))" (is "[_ = ?rhs] (mod _)") by simp
   1.286 +
   1.287 +  also have "[?rhs = (\<Sum>i\<le>p. if i \<le> 1 then (p choose i) * t ^ i * p ^ (i * (k - 1)) else 0)]
   1.288 +               (mod (p ^ Suc k))" (is "[sum ?f _ = sum ?g _] (mod _)")
   1.289 +  proof (intro cong_sum)
   1.290 +    fix i assume i: "i \<in> {..p}"
   1.291 +    consider "i \<le> 1" | "i = 2" | "i > 2" by force
   1.292 +    thus "[?f i = ?g i] (mod (p ^ Suc k))"
   1.293 +    proof cases
   1.294 +      assume i: "i > 2"
   1.295 +      have "Suc k \<le> 3 * (k - 1)"
   1.296 +        using \<open>k \<ge> 2\<close> by (simp add: algebra_simps)
   1.297 +      also have "3 * (k - 1) \<le> i * (k - 1)"
   1.298 +        using i by (intro mult_right_mono) auto
   1.299 +      finally have "p ^ Suc k dvd ?f i"
   1.300 +        by (intro dvd_mult le_imp_power_dvd)
   1.301 +      thus "[?f i = ?g i] (mod (p ^ Suc k))"
   1.302 +        by (simp add: cong_0_iff)
   1.303 +    next
   1.304 +      assume [simp]: "i = 2"
   1.305 +      have "?f i = p * (p - 1) div 2 * t\<^sup>2 * p ^ (2 * (k - 1))"
   1.306 +        using choose_two[of p] by simp
   1.307 +      also have "p * (p - 1) div 2 = (p - 1) div 2 * p"
   1.308 +        using \<open>odd p\<close> by (auto elim!: oddE)
   1.309 +      also have "\<dots> * t\<^sup>2 * p ^ (2 * (k - 1)) = (p - 1) div 2 * t\<^sup>2 * (p * p ^ (2 * (k - 1)))"
   1.310 +        by (simp add: algebra_simps)
   1.311 +      also have "p * p ^ (2 * (k - 1)) = p ^ (2 * k - 1)"
   1.312 +        using \<open>k \<ge> 2\<close> by (cases k) auto
   1.313 +      also have "p ^ Suc k dvd (p - 1) div 2 * t\<^sup>2 * p ^ (2 * k - 1)"
   1.314 +        using \<open>k \<ge> 2\<close> by (intro dvd_mult le_imp_power_dvd) auto
   1.315 +      finally show "[?f i = ?g i] (mod (p ^ Suc k))"
   1.316 +        by (simp add: cong_0_iff)
   1.317 +    qed auto
   1.318 +  qed
   1.319 +  also have "(\<Sum>i\<le>p. ?g i) = (\<Sum>i\<le>1. ?f i)"
   1.320 +    using p prime_gt_1_nat[of p] by (intro sum.mono_neutral_cong_right) auto
   1.321 +  also have "\<dots> = 1 + t * p ^ k"
   1.322 +    using choose_two[of p] \<open>k \<ge> 2\<close> by (cases k) simp_all
   1.323 +  finally have eq: "[g ^ totient (p ^ k) = 1 + t * p ^ k] (mod p ^ Suc k)" .
   1.324 +
   1.325 +  have "[g ^ totient (p ^ k) \<noteq> 1] (mod p ^ Suc k)"
   1.326 +  proof
   1.327 +    assume "[g ^ totient (p ^ k) = 1] (mod p ^ Suc k)"
   1.328 +    hence "[g ^ totient (p ^ k) - g ^ totient (p ^ k) = 1 + t * p ^ k - 1] (mod p ^ Suc k)"
   1.329 +      by (intro cong_diff_nat eq) auto
   1.330 +    hence "[t * p ^ k = 0] (mod p ^ Suc k)"
   1.331 +      by (simp add: cong_sym_eq)
   1.332 +    hence "p * p ^ k dvd t * p ^ k"
   1.333 +      by (simp add: cong_0_iff)
   1.334 +    hence "p dvd t" using \<open>p > 2\<close> by simp
   1.335 +    with \<open>\<not>p dvd t\<close> show False by contradiction
   1.336 +  qed
   1.337 +  thus ?case by simp
   1.338 +qed
   1.339 +
   1.340 +text \<open>
   1.341 +  We can now show that primitive roots modulo \<open>p\<close> with the above condition are
   1.342 +  indeed also primitive roots modulo $p^k$.
   1.343 +\<close>
   1.344 +proposition residue_primroot_prime_lift_iff:
   1.345 +  assumes p: "prime p" "odd p" and "residue_primroot p g"
   1.346 +  shows   "(\<forall>k>0. residue_primroot (p ^ k) g) \<longleftrightarrow> [g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
   1.347 +proof -
   1.348 +  from assms have g: "coprime p g" "ord p g = p - 1"
   1.349 +    by (auto simp: residue_primroot_def totient_prime)
   1.350 +  show ?thesis
   1.351 +  proof
   1.352 +    assume "\<forall>k>0. residue_primroot (p ^ k) g"
   1.353 +    hence "residue_primroot (p\<^sup>2) g" by auto
   1.354 +    hence "ord (p\<^sup>2) g = totient (p\<^sup>2)"
   1.355 +      by (simp_all add: residue_primroot_def)
   1.356 +    thus "[g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
   1.357 +      using g assms prime_gt_1_nat[of p]
   1.358 +      by (auto simp: ord_divides' totient_prime_power)
   1.359 +  next
   1.360 +    assume g': "[g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
   1.361 +
   1.362 +    have "residue_primroot (p ^ k) g" if "k > 0" for k
   1.363 +    proof (cases "k = 1")
   1.364 +      case False
   1.365 +      with that have k: "k > 1" by simp
   1.366 +      from g have coprime: "coprime (p ^ k) g"
   1.367 +        by (auto simp: totatives_def coprime_commute)
   1.368 +
   1.369 +      define t where "t = ord (p ^ k) g"
   1.370 +      have "[g ^ t = 1] (mod (p ^ k))"
   1.371 +        by (simp add: t_def ord_divides')
   1.372 +      also have "p ^ k = p * p ^ (k - 1)"
   1.373 +        using k by (cases k) auto
   1.374 +      finally have "[g ^ t = 1] (mod p)"
   1.375 +        by (rule cong_modulus_mult_nat)
   1.376 +      hence "totient p dvd t"
   1.377 +        using g p by (simp add: ord_divides' totient_prime)
   1.378 +      then obtain q where t: "t = totient p * q" by auto
   1.379 +
   1.380 +      have "t dvd totient (p ^ k)"
   1.381 +        using coprime by (simp add: t_def order_divides_totient)
   1.382 +      with t p k have "q dvd p ^ (k - 1)" using prime_gt_1_nat[of p]
   1.383 +        by (auto simp: totient_prime totient_prime_power)
   1.384 +      then obtain b where b: "b \<le> k - 1" "q = p ^ b"
   1.385 +        using divides_primepow_nat[of p q "k - 1"] p by auto
   1.386 +
   1.387 +      have "b = k - 1"
   1.388 +      proof (rule ccontr)
   1.389 +        assume "b \<noteq> k - 1"
   1.390 +        with b have "b < k - 1" by simp
   1.391 +        have "t = p ^ b * (p - 1)"
   1.392 +          using b p by (simp add: t totient_prime)
   1.393 +        also have "\<dots> dvd p ^ (k - 2) * (p - 1)"
   1.394 +          using \<open>b < k - 1\<close> by (intro mult_dvd_mono le_imp_power_dvd) auto
   1.395 +        also have "\<dots> = totient (p ^ (k - 1))"
   1.396 +          using k p by (simp add: totient_prime_power numeral_2_eq_2)
   1.397 +        finally have "[g ^ totient (p ^ (k - 1)) = 1] (mod (p ^ k))"
   1.398 +          by (simp add: ord_divides' t_def)
   1.399 +        with residue_primroot_power_prime_power_neq_1[of k p g] p k assms g' show False
   1.400 +          by auto
   1.401 +      qed
   1.402 +      hence "t = totient (p ^ k)"
   1.403 +        using p k by (simp add: t b totient_prime totient_prime_power)
   1.404 +      thus "residue_primroot (p ^ k) g"
   1.405 +        using g one_less_power[of p k] prime_gt_1_nat[of p] p k
   1.406 +        by (simp add: residue_primroot_def t_def)
   1.407 +    qed (use assms in auto)
   1.408 +    thus "\<forall>k>0. residue_primroot (p ^ k) g" by blast
   1.409 +  qed
   1.410 +qed
   1.411 +
   1.412 +text \<open>
   1.413 +  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
   1.414 +  fulfil the above assumption required for it to be liftable to $p^k$, we can use $g + p$, which
   1.415 +  is also a primitive root modulo \<open>p\<close> and \<^emph>\<open>does\<close> fulfil the assumption.
   1.416 +
   1.417 +  This shows that any modulus that is a power of an odd prime has a primitive root.
   1.418 +\<close>
   1.419 +theorem residue_primroot_odd_prime_power_exists:
   1.420 +  assumes p: "prime p" "odd p"
   1.421 +  obtains g where "\<forall>k>0. residue_primroot (p ^ k) g"
   1.422 +proof -
   1.423 +  obtain g where g: "residue_primroot p g"
   1.424 +    using prime_primitive_root_exists[of p] assms prime_gt_1_nat[of p] by auto
   1.425 +
   1.426 +  have "\<exists>g. residue_primroot p g \<and> [g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
   1.427 +  proof (cases "[g ^ (p - 1) = 1] (mod p\<^sup>2)")
   1.428 +    case True
   1.429 +    define g' where "g' = p + g"
   1.430 +    note g
   1.431 +    also have "residue_primroot p g \<longleftrightarrow> residue_primroot p g'"
   1.432 +      unfolding g'_def by (rule residue_primroot_cong) (auto simp: cong_def)
   1.433 +    finally have g': "residue_primroot p g'" .
   1.434 +
   1.435 +    have "[g' ^ (p - 1) = (\<Sum>k\<le>p-1. ((p-1) choose k) * g ^ (p - Suc k) * p ^ k)] (mod p\<^sup>2)"
   1.436 +      (is "[_ = ?rhs] (mod _)") by (simp add: g'_def binomial mult_ac)
   1.437 +    also have "[?rhs = (\<Sum>k\<le>p-1. if k \<le> 1 then ((p-1) choose k) *
   1.438 +                                   g ^ (p - Suc k) * p ^ k else 0)] (mod p\<^sup>2)"
   1.439 +      (is "[sum ?f _ = sum ?g _] (mod _)")
   1.440 +    proof (intro cong_sum)
   1.441 +      fix k assume "k \<in> {..p-1}"
   1.442 +      show "[?f k = ?g k] (mod p\<^sup>2)"
   1.443 +      proof (cases "k \<le> 1")
   1.444 +        case False
   1.445 +        have "p\<^sup>2 dvd ?f k"
   1.446 +          using False by (intro dvd_mult le_imp_power_dvd) auto
   1.447 +        thus ?thesis using False by (simp add: cong_0_iff)
   1.448 +      qed auto
   1.449 +    qed
   1.450 +    also have "sum ?g {..p-1} = sum ?f {0, 1}"
   1.451 +      using prime_gt_1_nat[of p] p by (intro sum.mono_neutral_cong_right) auto
   1.452 +    also have "\<dots> = g ^ (p - 1) + p * (p - 1) * g ^ (p - 2)"
   1.453 +      using p by (simp add: numeral_2_eq_2)
   1.454 +    also have "[g ^ (p - 1) + p * (p - 1) * g ^ (p - 2) = 1 + p * (p - 1) * g ^ (p - 2)] (mod p\<^sup>2)"
   1.455 +      by (intro cong_add True) auto
   1.456 +    finally have "[g' ^ (p - 1) = 1 + p * (p - 1) * g ^ (p - 2)] (mod p\<^sup>2)" .
   1.457 +
   1.458 +    moreover have "[1 + p * (p - 1) * g ^ (p - 2) \<noteq> 1] (mod p\<^sup>2)"
   1.459 +    proof
   1.460 +      assume "[1 + p * (p - 1) * g ^ (p - 2) = 1] (mod p\<^sup>2)"
   1.461 +      hence "[1 + p * (p - 1) * g ^ (p - 2) - 1 = 1 - 1] (mod p\<^sup>2)"
   1.462 +        by (intro cong_diff_nat) auto
   1.463 +      hence "p * p dvd p * ((p - 1) * g ^ (p - 2))"
   1.464 +        by (auto simp: cong_0_iff power2_eq_square)
   1.465 +      hence "p dvd (p - 1) * g ^ (p - 2)"
   1.466 +        using p by simp
   1.467 +      hence "p dvd g ^ (p - 2)"
   1.468 +        using p dvd_imp_le[of p "p - Suc 0"] prime_gt_1_nat[of p]
   1.469 +        by (auto simp: prime_dvd_mult_iff)
   1.470 +      also have "\<dots> dvd g ^ (p - 1)"
   1.471 +        by (intro le_imp_power_dvd) auto
   1.472 +      finally have "[g ^ (p - 1) = 0] (mod p)"
   1.473 +        by (simp add: cong_0_iff)
   1.474 +      hence "[0 = g ^ (p - 1)] (mod p)"
   1.475 +        by (simp add: cong_sym_eq)
   1.476 +
   1.477 +      also from \<open>residue_primroot p g\<close> have "[g ^ (p - 1) = 1] (mod p)"
   1.478 +        using p by (auto simp: residue_primroot_def ord_divides' totient_prime)
   1.479 +      finally have "[0 = 1] (mod p)" .
   1.480 +      thus False using prime_gt_1_nat[of p] p by (simp add: cong_def)
   1.481 +    qed
   1.482 +
   1.483 +    ultimately have "[g' ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
   1.484 +      by (simp add: cong_def)
   1.485 +    thus "\<exists>g. residue_primroot p g \<and> [g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
   1.486 +      using g' by blast    
   1.487 +  qed (use g in auto)
   1.488 +  thus ?thesis
   1.489 +    using residue_primroot_prime_lift_iff[OF assms] that by blast
   1.490 +qed
   1.491 +
   1.492 +
   1.493 +subsection \<open>Carmichael's function\<close>
   1.494 +
   1.495 +text \<open>
   1.496 +  Carmichael's function $\lambda(n)$ gives the LCM of the orders of all elements in the
   1.497 +  residue ring modulo $n$ -- or, equivalently, the maximum order, as we will show later.
   1.498 +  Algebraically speaking, it is the exponent of the multiplicative group
   1.499 +  $(\mathbb{Z}/n\mathbb{Z})^*$.
   1.500 +
   1.501 +  It is not to be confused with Liouville's function, which is also denoted by $\lambda(n)$.
   1.502 +\<close>
   1.503 +definition Carmichael where
   1.504 +  "Carmichael n = (LCM a \<in> totatives n. ord n a)"
   1.505 +
   1.506 +lemma Carmichael_0 [simp]: "Carmichael 0 = 1"
   1.507 +  by (simp add: Carmichael_def)
   1.508 +
   1.509 +lemma Carmichael_1 [simp]: "Carmichael 1 = 1"
   1.510 +  by (simp add: Carmichael_def)
   1.511 +
   1.512 +lemma Carmichael_Suc_0 [simp]: "Carmichael (Suc 0) = 1"
   1.513 +  by (simp add: Carmichael_def)
   1.514 +
   1.515 +lemma ord_dvd_Carmichael:
   1.516 +  assumes "n > 1" "coprime n k"
   1.517 +  shows   "ord n k dvd Carmichael n"
   1.518 +proof -
   1.519 +  have "k mod n \<in> totatives n"
   1.520 +    using assms by (auto simp: totatives_def coprime_commute intro!: Nat.gr0I)
   1.521 +  hence "ord n (k mod n) dvd Carmichael n"
   1.522 +    by (simp add: Carmichael_def del: ord_mod)
   1.523 +  thus ?thesis by simp
   1.524 +qed
   1.525 +
   1.526 +lemma Carmichael_divides:
   1.527 +  assumes "Carmichael n dvd k" "coprime n a"
   1.528 +  shows   "[a ^ k = 1] (mod n)"
   1.529 +proof (cases "n < 2 \<or> a = 1")
   1.530 +  case False
   1.531 +  hence "ord n a dvd Carmichael n"
   1.532 +    using False assms by (intro ord_dvd_Carmichael) auto
   1.533 +  also have "\<dots> dvd k" by fact
   1.534 +  finally have "ord n a dvd k" .
   1.535 +  thus ?thesis using ord_divides by auto
   1.536 +next
   1.537 +  case True
   1.538 +  then consider "a = 1" | "n = 0" | "n = 1" by force
   1.539 +  thus ?thesis using assms by cases auto
   1.540 +qed
   1.541 +
   1.542 +lemma Carmichael_dvd_totient: "Carmichael n dvd totient n"
   1.543 +  unfolding Carmichael_def
   1.544 +proof (intro Lcm_least, safe)
   1.545 +  fix a assume "a \<in> totatives n"
   1.546 +  hence "[a ^ totient n = 1] (mod n)"
   1.547 +    by (intro euler_theorem) (auto simp: totatives_def)
   1.548 +  thus "ord n a dvd totient n"
   1.549 +    using ord_divides by blast
   1.550 +qed
   1.551 +
   1.552 +lemma Carmichael_dvd_mono_coprime:
   1.553 +  assumes "coprime m n" "m > 1" "n > 1"
   1.554 +  shows   "Carmichael m dvd Carmichael (m * n)"
   1.555 +  unfolding Carmichael_def[of m]
   1.556 +proof (intro Lcm_least, safe)
   1.557 +  fix x assume x: "x \<in> totatives m"
   1.558 +  from assms have "totatives n \<noteq> {}" by simp
   1.559 +  then obtain y where y: "y \<in> totatives n" by blast
   1.560 +
   1.561 +  from binary_chinese_remainder_nat[OF assms(1), of x y]
   1.562 +  obtain z where z: "[z = x] (mod m)" "[z = y] (mod n)" by blast
   1.563 +  have z': "coprime z n" "coprime z m"
   1.564 +    by (rule cong_imp_coprime; use x y z in \<open>force simp: totatives_def cong_sym_eq\<close>)+
   1.565 +
   1.566 +  from z have "ord m x = ord m z"
   1.567 +    by (intro ord_cong) (auto simp: cong_sym_eq)
   1.568 +  also have "ord m z dvd ord (m * n) z"
   1.569 +    using assms by (auto simp: ord_modulus_mult_coprime)
   1.570 +  also from z' assms have "\<dots> dvd Carmichael (m * n)"
   1.571 +    by (intro ord_dvd_Carmichael) (auto simp: coprime_commute intro!:one_less_mult)
   1.572 +  finally show "ord m x dvd Carmichael (m * n)" .
   1.573 +qed
   1.574 +
   1.575 +text \<open>
   1.576 +  $\lambda$ distributes over the product of coprime numbers similarly to $\varphi$, but
   1.577 +  with LCM instead of multiplication:
   1.578 +\<close>
   1.579 +lemma Carmichael_mult_coprime:
   1.580 +  assumes "coprime m n"
   1.581 +  shows   "Carmichael (m * n) = lcm (Carmichael m) (Carmichael n)"
   1.582 +proof (cases "m \<le> 1 \<or> n \<le> 1")
   1.583 +  case True
   1.584 +  hence "m = 0 \<or> n = 0 \<or> m = 1 \<or> n = 1" by force
   1.585 +  thus ?thesis using assms by auto
   1.586 +next
   1.587 +  case False
   1.588 +  show ?thesis
   1.589 +  proof (rule dvd_antisym)
   1.590 +    show "Carmichael (m * n) dvd lcm (Carmichael m) (Carmichael n)"
   1.591 +      unfolding Carmichael_def[of "m * n"]
   1.592 +    proof (intro Lcm_least, safe)
   1.593 +      fix x assume x: "x \<in> totatives (m * n)"
   1.594 +      have "ord (m * n) x = lcm (ord m x) (ord n x)"
   1.595 +        using assms x by (subst ord_modulus_mult_coprime) (auto simp: coprime_commute totatives_def)
   1.596 +      also have "\<dots> dvd lcm (Carmichael m) (Carmichael n)"
   1.597 +        using False x
   1.598 +        by (intro lcm_mono ord_dvd_Carmichael) (auto simp: totatives_def coprime_commute)
   1.599 +      finally show "ord (m * n) x dvd \<dots>" .
   1.600 +    qed
   1.601 +  next
   1.602 +    show "lcm (Carmichael m) (Carmichael n) dvd Carmichael (m * n)"
   1.603 +      using Carmichael_dvd_mono_coprime[of m n]
   1.604 +            Carmichael_dvd_mono_coprime[of n m] assms False
   1.605 +      by (auto intro!: lcm_least simp: coprime_commute mult.commute)
   1.606 +  qed
   1.607 +qed
   1.608 +
   1.609 +lemma Carmichael_pos [simp, intro]: "Carmichael n > 0"
   1.610 +  by (auto simp: Carmichael_def ord_eq_0 totatives_def coprime_commute intro!: Nat.gr0I)
   1.611 +
   1.612 +lemma Carmichael_nonzero [simp]: "Carmichael n \<noteq> 0"
   1.613 +  by simp
   1.614 +
   1.615 +lemma power_Carmichael_eq_1:
   1.616 +  assumes "n > 1" "coprime n x"
   1.617 +  shows   "[x ^ Carmichael n = 1] (mod n)"
   1.618 +  using ord_dvd_Carmichael[of n x] assms
   1.619 +  by (auto simp: ord_divides')
   1.620 +
   1.621 +lemma Carmichael_2 [simp]: "Carmichael 2 = 1"
   1.622 +  using Carmichael_dvd_totient[of 2] by simp
   1.623 +
   1.624 +lemma Carmichael_4 [simp]: "Carmichael 4 = 2"
   1.625 +proof -
   1.626 +  have "Carmichael 4 dvd 2"
   1.627 +    using Carmichael_dvd_totient[of 4] by simp
   1.628 +  hence "Carmichael 4 \<le> 2" by (rule dvd_imp_le) auto
   1.629 +  moreover have "Carmichael 4 \<noteq> 1"
   1.630 +    using power_Carmichael_eq_1[of "4::nat" 3]
   1.631 +    unfolding coprime_iff_gcd_eq_1 by (auto simp: gcd_non_0_nat cong_def)
   1.632 +  ultimately show ?thesis
   1.633 +    using Carmichael_pos[of 4] by linarith
   1.634 +qed
   1.635 +
   1.636 +lemma residue_primroot_Carmichael:
   1.637 +  assumes "residue_primroot n g"
   1.638 +  shows   "Carmichael n = totient n"
   1.639 +proof (cases "n = 1")
   1.640 +  case False
   1.641 +  show ?thesis
   1.642 +  proof (intro dvd_antisym Carmichael_dvd_totient)
   1.643 +    have "ord n g dvd Carmichael n"
   1.644 +      using assms False by (intro ord_dvd_Carmichael) (auto simp: residue_primroot_def)
   1.645 +    thus "totient n dvd Carmichael n"
   1.646 +      using assms by (auto simp: residue_primroot_def)
   1.647 +  qed
   1.648 +qed auto
   1.649 +
   1.650 +lemma Carmichael_odd_prime_power:
   1.651 +  assumes "prime p" "odd p" "k > 0"
   1.652 +  shows   "Carmichael (p ^ k) = p ^ (k - 1) * (p - 1)"
   1.653 +proof -
   1.654 +  from assms obtain g where "residue_primroot (p ^ k) g"
   1.655 +    using residue_primroot_odd_prime_power_exists[of p] assms by metis
   1.656 +  hence "Carmichael (p ^ k) = totient (p ^ k)"
   1.657 +    by (intro residue_primroot_Carmichael[of "p ^ k" g]) auto
   1.658 +  with assms show ?thesis by (simp add: totient_prime_power)
   1.659 +qed
   1.660 +
   1.661 +lemma Carmichael_prime:
   1.662 +  assumes "prime p"
   1.663 +  shows   "Carmichael p = p - 1"
   1.664 +proof (cases "even p")
   1.665 +  case True
   1.666 +  with assms have "p = 2"
   1.667 +    using primes_dvd_imp_eq two_is_prime_nat by blast
   1.668 +  thus ?thesis by simp
   1.669 +next
   1.670 +  case False
   1.671 +  with Carmichael_odd_prime_power[of p 1] assms show ?thesis by simp
   1.672 +qed
   1.673 +  
   1.674 +lemma Carmichael_twopow_ge_8:
   1.675 +  assumes "k \<ge> 3"
   1.676 +  shows   "Carmichael (2 ^ k) = 2 ^ (k - 2)"
   1.677 +proof (intro dvd_antisym)
   1.678 +  have "2 ^ (k - 2) = ord (2 ^ k) (3 :: nat)"
   1.679 +    using ord_twopow_3_5[of k 3] assms by simp
   1.680 +  also have "\<dots> dvd Carmichael (2 ^ k)"
   1.681 +    using assms one_less_power[of "2::nat" k] by (intro ord_dvd_Carmichael) auto
   1.682 +  finally show "2 ^ (k - 2) dvd \<dots>" .
   1.683 +next
   1.684 +  show "Carmichael (2 ^ k) dvd 2 ^ (k - 2)"
   1.685 +    unfolding Carmichael_def
   1.686 +  proof (intro Lcm_least, safe)
   1.687 +    fix x assume "x \<in> totatives (2 ^ k)"
   1.688 +    hence "odd x" by (auto simp: totatives_def)
   1.689 +    hence "[x ^ 2 ^ (k - 2) = 1] (mod 2 ^ k)"
   1.690 +      using assms ord_twopow_aux[of k x] by auto
   1.691 +    thus "ord (2 ^ k) x dvd 2 ^ (k - 2)"
   1.692 +      by (simp add: ord_divides')
   1.693 +  qed
   1.694 +qed
   1.695 +
   1.696 +lemma Carmichael_twopow:
   1.697 +  "Carmichael (2 ^ k) = (if k \<le> 2 then 2 ^ (k - 1) else 2 ^ (k - 2))"
   1.698 +proof -
   1.699 +  have "k = 0 \<or> k = 1 \<or> k = 2 \<or> k \<ge> 3" by linarith
   1.700 +  thus ?thesis by (auto simp: Carmichael_twopow_ge_8)
   1.701 +qed
   1.702 +
   1.703 +lemma Carmichael_prime_power:
   1.704 +  assumes "prime p" "k > 0"
   1.705 +  shows   "Carmichael (p ^ k) =
   1.706 +             (if p = 2 \<and> k > 2 then 2 ^ (k - 2) else p ^ (k - 1) * (p - 1))"
   1.707 +proof (cases "p = 2")
   1.708 +  case True
   1.709 +  thus ?thesis by (simp add: Carmichael_twopow)
   1.710 +next
   1.711 +  case False
   1.712 +  with assms have "odd p" "p > 2"
   1.713 +    using prime_odd_nat[of p] prime_gt_1_nat[of p] by auto
   1.714 +  thus ?thesis
   1.715 +    using assms Carmichael_odd_prime_power[of p k] by simp
   1.716 +qed
   1.717 +
   1.718 +lemma Carmichael_prod_coprime:
   1.719 +  assumes "finite A" "\<And>i j. i \<in> A \<Longrightarrow> j \<in> A \<Longrightarrow> i \<noteq> j \<Longrightarrow> coprime (f i) (f j)"
   1.720 +  shows   "Carmichael (\<Prod>i\<in>A. f i) = (LCM i\<in>A. Carmichael (f i))"
   1.721 +  using assms by (induction A rule: finite_induct)
   1.722 +                 (simp, simp, subst Carmichael_mult_coprime[OF prod_coprime_right], auto)
   1.723 +
   1.724 +text \<open>
   1.725 +  Since $\lambda$ distributes over coprime factors and we know the value of $\lambda(p^k)$
   1.726 +  for prime $p$, we can now give a closed formula for $\lambda(n)$ in terms of the prime
   1.727 +  factorisation of $n$:
   1.728 +\<close>
   1.729 +theorem Carmichael_closed_formula:
   1.730 +  "Carmichael n =
   1.731 +     (LCM p\<in>prime_factors n. let k = multiplicity p n
   1.732 +                             in  if p = 2 \<and> k > 2 then 2 ^ (k - 2) else p ^ (k - 1) * (p - 1))"
   1.733 +  (is "_ = Lcm ?A")
   1.734 +proof (cases "n = 0")
   1.735 +  case False
   1.736 +  hence "n = (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n)"
   1.737 +    using prime_factorization_nat by blast
   1.738 +  also have "Carmichael \<dots> =
   1.739 +               (LCM p\<in>prime_factors n. Carmichael (p ^ multiplicity p n))"
   1.740 +    by (subst Carmichael_prod_coprime) (auto simp: in_prime_factors_iff primes_coprime)
   1.741 +  also have "(\<lambda>p. Carmichael (p ^ multiplicity p n)) ` prime_factors n = ?A"
   1.742 +    by (intro image_cong)
   1.743 +       (auto simp: Let_def Carmichael_prime_power prime_factors_multiplicity)
   1.744 +  finally show ?thesis .
   1.745 +qed auto
   1.746 +
   1.747 +corollary even_Carmichael:
   1.748 +  assumes "n > 2"
   1.749 +  shows   "even (Carmichael n)"
   1.750 +proof (cases "\<exists>k. n = 2 ^ k")
   1.751 +  case True
   1.752 +  then obtain k where [simp]: "n = 2 ^ k" by auto
   1.753 +  from assms have "k \<noteq> 0" "k \<noteq> 1" by (auto intro!: Nat.gr0I)
   1.754 +  hence "k \<ge> 2" by auto
   1.755 +  thus ?thesis by (auto simp: Carmichael_twopow)
   1.756 +next
   1.757 +  case False
   1.758 +  from assms have "n \<noteq> 0" by auto
   1.759 +  from False have "\<exists>p\<in>prime_factors n. p \<noteq> 2"
   1.760 +    using assms Ex_other_prime_factor[of n 2] by auto
   1.761 +  from divide_out_primepow_ex[OF \<open>n \<noteq> 0\<close> this] guess p k n' . note p = this
   1.762 +  from p have coprime: "coprime (p ^ k) n'"
   1.763 +    using p prime_imp_coprime by auto
   1.764 +  have "odd p"
   1.765 +    using p primes_dvd_imp_eq[of 2 p] by auto
   1.766 +  have "even (Carmichael (p ^ k))"
   1.767 +    using p \<open>odd p\<close> by (auto simp: Carmichael_prime_power)
   1.768 +  with p coprime show ?thesis
   1.769 +    by (auto simp: Carmichael_mult_coprime intro!: dvd_lcmI1)
   1.770 +qed
   1.771 +
   1.772 +lemma eval_Carmichael:
   1.773 +  assumes "prime_factorization n = A"
   1.774 +  shows     "Carmichael n = (LCM p \<in> set_mset A.
   1.775 +               let k = count A p in if p = 2 \<and> k > 2 then 2 ^ (k - 2) else p ^ (k - 1) * (p - 1))"
   1.776 +  unfolding assms [symmetric] Carmichael_closed_formula
   1.777 +  by (intro arg_cong[where f = Lcm] image_cong) (auto simp: Let_def count_prime_factorization)
   1.778 +
   1.779 +text \<open>
   1.780 +  Any residue ring always contains a $\lambda$-root, i.\,e.\ an element whose
   1.781 +  order is $\lambda(n)$.
   1.782 +\<close>
   1.783 +theorem Carmichael_root_exists:
   1.784 +  assumes "n > (0::nat)"
   1.785 +  obtains g where "g \<in> totatives n" and "ord n g = Carmichael n"
   1.786 +proof (cases "n = 1")
   1.787 +  case True
   1.788 +  thus ?thesis by (intro that[of 1]) (auto simp: totatives_def)
   1.789 +next
   1.790 +  case False
   1.791 +  have primepow: "\<exists>g. coprime (p ^ k) g \<and> ord (p ^ k) g = Carmichael (p ^ k)"
   1.792 +    if pk: "prime p" "k > 0" for p k
   1.793 +  proof (cases "p = 2")
   1.794 +    case [simp]: True
   1.795 +    from \<open>k > 0\<close> consider "k = 1" | "k = 2" | "k \<ge> 3" by force
   1.796 +    thus ?thesis
   1.797 +    proof cases
   1.798 +      assume "k = 1"
   1.799 +      thus ?thesis by (intro exI[of _ 1]) auto
   1.800 +    next
   1.801 +      assume [simp]: "k = 2"
   1.802 +      have "coprime 4 (3::nat)"
   1.803 +        by (auto simp: coprime_iff_gcd_eq_1 gcd_non_0_nat)
   1.804 +      thus ?thesis by (intro exI[of _ 3]) auto
   1.805 +    next
   1.806 +      assume k: "k \<ge> 3"
   1.807 +      have "coprime (2 ^ k :: nat) 3" by auto
   1.808 +      thus ?thesis using k
   1.809 +        by (intro exI[of _ 3]) (auto simp: ord_twopow_3_5 Carmichael_twopow)
   1.810 +    qed
   1.811 +  next
   1.812 +    case False
   1.813 +    hence "odd p" using \<open>prime p\<close>
   1.814 +      using primes_dvd_imp_eq two_is_prime_nat by blast
   1.815 +    then obtain g where "residue_primroot (p ^ k) g"
   1.816 +      using residue_primroot_odd_prime_power_exists[of p] pk by metis
   1.817 +    thus ?thesis using False pk
   1.818 +      by (intro exI[of _ g])
   1.819 +         (auto simp: Carmichael_prime_power residue_primroot_def totient_prime_power)
   1.820 +  qed
   1.821 +
   1.822 +  define P where "P = prime_factors n"
   1.823 +  define k where "k = (\<lambda>p. multiplicity p n)"
   1.824 +  have "\<forall>p\<in>P. \<exists>g. coprime (p ^ k p) g \<and> ord (p ^ k p) g = Carmichael (p ^ k p)"
   1.825 +    using primepow by (auto simp: P_def k_def prime_factors_multiplicity)
   1.826 +  hence "\<exists>g. \<forall>p\<in>P. coprime (p ^ k p) (g p) \<and> ord (p ^ k p) (g p) = Carmichael (p ^ k p)"
   1.827 +    by (subst (asm) bchoice_iff)
   1.828 +  then obtain g where g: "\<And>p. p \<in> P \<Longrightarrow> coprime (p ^ k p) (g p)"
   1.829 +                         "\<And>p. p \<in> P \<Longrightarrow> ord (p ^ k p) (g p) = Carmichael (p ^ k p)" by metis
   1.830 +  have "\<exists>x. \<forall>i\<in>P. [x = g i] (mod i ^ k i)"
   1.831 +    by (intro chinese_remainder_nat)
   1.832 +       (auto simp: P_def k_def in_prime_factors_iff primes_coprime)
   1.833 +  then obtain x where x: "\<And>p. p \<in> P \<Longrightarrow> [x = g p] (mod p ^ k p)" by metis
   1.834 +
   1.835 +  have "n = (\<Prod>p\<in>P. p ^ k p)"
   1.836 +    using assms unfolding P_def k_def by (rule prime_factorization_nat)
   1.837 +  also have "ord \<dots> x = (LCM p\<in>P. ord (p ^ k p) x)"
   1.838 +    by (intro ord_modulus_prod_coprime) (auto simp: P_def in_prime_factors_iff primes_coprime)
   1.839 +  also have "(\<lambda>p. ord (p ^ k p) x) ` P = (\<lambda>p. ord (p ^ k p) (g p)) ` P"
   1.840 +    by (intro image_cong ord_cong x) auto
   1.841 +  also have "\<dots> = (\<lambda>p. Carmichael (p ^ k p)) ` P"
   1.842 +    by (intro image_cong g) auto
   1.843 +  also have "Lcm \<dots> = Carmichael (\<Prod>p\<in>P. p ^ k p)"
   1.844 +    by (intro Carmichael_prod_coprime [symmetric])
   1.845 +       (auto simp: P_def in_prime_factors_iff primes_coprime)
   1.846 +  also have "(\<Prod>p\<in>P. p ^ k p) = n"
   1.847 +    using assms unfolding P_def k_def by (rule prime_factorization_nat [symmetric])
   1.848 +  finally have "ord n x = Carmichael n" .
   1.849 +  moreover from this have "coprime n x"
   1.850 +    by (cases "coprime n x") (auto split: if_splits)
   1.851 +  ultimately show ?thesis using assms False
   1.852 +    by (intro that[of "x mod n"])
   1.853 +       (auto simp: totatives_def coprime_commute coprime_absorb_left intro!: Nat.gr0I)
   1.854 +qed
   1.855 +
   1.856 +text \<open>
   1.857 +  This also means that the Carmichael number is not only the LCM of the orders
   1.858 +  of the elements of the residue ring, but indeed the maximum of the orders.
   1.859 +\<close>
   1.860 +lemma Carmichael_altdef:
   1.861 +  "Carmichael n = (if n = 0 then 1 else Max (ord n ` totatives n))"
   1.862 +proof (cases "n = 0")
   1.863 +  case False
   1.864 +  have "Carmichael n = Max (ord n ` totatives n)"
   1.865 +  proof (intro antisym Max.boundedI Max.coboundedI)
   1.866 +    fix k assume k: "k \<in> ord n ` totatives n"
   1.867 +    thus "k \<le> Carmichael n"
   1.868 +    proof (cases "n = 1")
   1.869 +      case False
   1.870 +      with \<open>n \<noteq> 0\<close> have "n > 1" by linarith
   1.871 +      thus ?thesis using k \<open>n \<noteq> 0\<close>
   1.872 +        by (intro dvd_imp_le)
   1.873 +           (auto intro!: ord_dvd_Carmichael simp: totatives_def coprime_commute)
   1.874 +    qed auto
   1.875 +  next
   1.876 +    obtain g where "g \<in> totatives n" and "ord n g = Carmichael n"
   1.877 +      using Carmichael_root_exists[of n] \<open>n \<noteq> 0\<close> by auto
   1.878 +    thus "Carmichael n \<in> ord n ` totatives n" by force
   1.879 +  qed (use \<open>n \<noteq> 0\<close> in auto)
   1.880 +  thus ?thesis using False by simp
   1.881 +qed auto
   1.882 +
   1.883 +
   1.884 +subsection \<open>Existence of primitive roots for general moduli\<close>
   1.885 +
   1.886 +text \<open>
   1.887 +  We now related Carmichael's function to the existence of primitive roots and, in the end,
   1.888 +  use this to show precisely which moduli have primitive roots and which do not.
   1.889 +
   1.890 +  The first criterion for the existence of a primitive root is this: A primitive root modulo $n$
   1.891 +  exists iff $\lambda(n) = \varphi(n)$.
   1.892 +\<close>
   1.893 +lemma Carmichael_eq_totient_imp_primroot:
   1.894 +  assumes "n > 0" and "Carmichael n = totient n"
   1.895 +  shows   "\<exists>g. residue_primroot n g"
   1.896 +proof -
   1.897 +  from \<open>n > 0\<close> obtain g where "g \<in> totatives n" and "ord n g = Carmichael n"
   1.898 +    using Carmichael_root_exists[of n] by metis
   1.899 +  with assms show ?thesis by (auto simp: residue_primroot_def totatives_def coprime_commute)
   1.900 +qed
   1.901 +
   1.902 +theorem residue_primroot_iff_Carmichael:
   1.903 +  "(\<exists>g. residue_primroot n g) \<longleftrightarrow> Carmichael n = totient n \<and> n > 0"
   1.904 +proof safe
   1.905 +  fix g assume g: "residue_primroot n g"
   1.906 +  thus "n > 0" by (auto simp: residue_primroot_def)
   1.907 +  have "coprime n g" by (rule ccontr) (use g in \<open>auto simp: residue_primroot_def\<close>)
   1.908 +
   1.909 +  show "Carmichael n = totient n"
   1.910 +  proof (cases "n = 1")
   1.911 +    case False
   1.912 +    with \<open>n > 0\<close> have "n > 1" by auto
   1.913 +    with \<open>coprime n g\<close> have "ord n g dvd Carmichael n"
   1.914 +      by (intro ord_dvd_Carmichael) auto
   1.915 +    thus ?thesis using g by (intro dvd_antisym Carmichael_dvd_totient)
   1.916 +                            (auto simp: residue_primroot_def)
   1.917 +  qed auto
   1.918 +qed (use Carmichael_eq_totient_imp_primroot[of n] in auto)
   1.919 +
   1.920 +text \<open>
   1.921 +  Any primitive root modulo $mn$ for coprime $m$, $n$ is also a primitive root modulo $m$ and $n$.
   1.922 +  The converse does not hold in general.
   1.923 +\<close>
   1.924 +lemma residue_primroot_modulus_mult_coprimeD:
   1.925 +  assumes "coprime m n" and "residue_primroot (m * n) g"
   1.926 +  shows   "residue_primroot m g" "residue_primroot n g"
   1.927 +proof -
   1.928 +  have *: "m > 0" "n > 0" "coprime m g" "coprime n g"
   1.929 +          "lcm (ord m g) (ord n g) = totient m * totient n"
   1.930 +    using assms
   1.931 +    by (auto simp: residue_primroot_def ord_modulus_mult_coprime totient_mult_coprime)
   1.932 +
   1.933 +  define a b where "a = totient m div ord m g" and "b = totient n div ord n g"
   1.934 +  have ab: "totient m = ord m g * a" "totient n = ord n g * b"
   1.935 +    using * by (auto simp: a_def b_def order_divides_totient)
   1.936 +
   1.937 +  have "a = 1" "b = 1" "coprime (ord m g) (ord n g)"
   1.938 +    unfolding coprime_iff_gcd_eq_1 using * by (auto simp: ab lcm_nat_def dvd_div_eq_mult ord_eq_0)
   1.939 +  with ab and * show "residue_primroot m g" "residue_primroot n g"
   1.940 +    by (auto simp: residue_primroot_def)
   1.941 +qed
   1.942 +
   1.943 +text \<open>
   1.944 +  If a primitive root modulo $mn$ exists for coprime $m, n$, then $\lambda(m)$ and $\lambda(n)$
   1.945 +  must also be coprime. This is helpful in establishing that there are no primitive roots
   1.946 +  modulo $mn$ by showing e.\,g.\ that $\lambda(m)$ and $\lambda(n)$ are both even.
   1.947 +\<close>
   1.948 +lemma residue_primroot_modulus_mult_coprime_imp_Carmichael_coprime:
   1.949 +  assumes "coprime m n" and "residue_primroot (m * n) g"
   1.950 +  shows   "coprime (Carmichael m) (Carmichael n)"
   1.951 +proof -
   1.952 +  from residue_primroot_modulus_mult_coprimeD[OF assms]
   1.953 +    have *: "residue_primroot m g" "residue_primroot n g" by auto
   1.954 +  hence [simp]: "Carmichael m = totient m" "Carmichael n = totient n"
   1.955 +    by (simp_all add: residue_primroot_Carmichael)
   1.956 +  from * have mn: "m > 0" "n > 0" by (auto simp: residue_primroot_def)
   1.957 +  
   1.958 +  from assms have "Carmichael (m * n) = totient (m * n) \<and> n > 0"
   1.959 +    using residue_primroot_iff_Carmichael[of "m * n"] by auto
   1.960 +  with assms have "lcm (totient m) (totient n) = totient m * totient n"
   1.961 +    by (simp add: Carmichael_mult_coprime totient_mult_coprime)
   1.962 +  thus ?thesis unfolding coprime_iff_gcd_eq_1 using mn
   1.963 +    by (simp add: lcm_nat_def dvd_div_eq_mult)
   1.964 +qed
   1.965 +  
   1.966 +text \<open>
   1.967 +  The following moduli are precisely those that have primitive roots.
   1.968 +\<close>
   1.969 +definition cyclic_moduli :: "nat set" where
   1.970 +  "cyclic_moduli = {1, 2, 4} \<union> {p ^ k |p k. prime p \<and> odd p \<and> k > 0} \<union>
   1.971 +                     {2 * p ^ k |p k. prime p \<and> odd p \<and> k > 0}"
   1.972 +
   1.973 +theorem residue_primroot_iff_in_cyclic_moduli:
   1.974 +  "(\<exists>g. residue_primroot m g) \<longleftrightarrow> m \<in> cyclic_moduli"
   1.975 +proof -
   1.976 +  have "(\<exists>g. residue_primroot m g)" if "m \<in> cyclic_moduli"
   1.977 +  using that unfolding cyclic_moduli_def
   1.978 +  by (intro Carmichael_eq_totient_imp_primroot)
   1.979 +     (auto dest: prime_gt_0_nat simp: Carmichael_prime_power totient_prime_power
   1.980 +                 Carmichael_mult_coprime totient_mult_coprime)
   1.981 +
   1.982 +  moreover have "\<not>(\<exists>g. residue_primroot m g)" if "m \<notin> cyclic_moduli"
   1.983 +  proof (cases "m = 0")
   1.984 +    case False
   1.985 +    with that have [simp]: "m > 0" "m \<noteq> 1" by (auto simp: cyclic_moduli_def)
   1.986 +    show ?thesis
   1.987 +    proof (cases "\<exists>k. m = 2 ^ k")
   1.988 +      case True
   1.989 +      then obtain k where [simp]: "m = 2 ^ k" by auto
   1.990 +      with that have "k \<noteq> 0 \<and> k \<noteq> 1 \<and> k \<noteq> 2" by (auto simp: cyclic_moduli_def)
   1.991 +      hence "k \<ge> 3" by auto
   1.992 +      thus ?thesis by (subst residue_primroot_iff_Carmichael)
   1.993 +                      (auto simp: Carmichael_twopow totient_prime_power)
   1.994 +    next
   1.995 +      case False
   1.996 +      hence "\<exists>p\<in>prime_factors m. p \<noteq> 2"
   1.997 +        using Ex_other_prime_factor[of m 2] by auto
   1.998 +      from divide_out_primepow_ex[OF \<open>m \<noteq> 0\<close> this]
   1.999 +      obtain p k m' where p: "p \<noteq> 2" "prime p" "p dvd m" "\<not>p dvd m'" "0 < k" "m = p ^ k * m'"
  1.1000 +        by metis
  1.1001 +      have "odd p"
  1.1002 +        using p primes_dvd_imp_eq[of 2 p] by auto
  1.1003 +      from p have coprime: "coprime (p ^ k) m'"
  1.1004 +        using p prime_imp_coprime by auto
  1.1005 +      have "m \<in> cyclic_moduli" if "m' = 1"
  1.1006 +        using that p \<open>odd p\<close> by (auto simp: cyclic_moduli_def)
  1.1007 +      moreover have "m \<in> cyclic_moduli" if "m' = 2"
  1.1008 +      proof -
  1.1009 +        have "m = 2 * p ^ k" using p that by (simp add: mult.commute)
  1.1010 +        thus "m \<in> cyclic_moduli" using p \<open>odd p\<close>
  1.1011 +          unfolding cyclic_moduli_def by blast
  1.1012 +      qed
  1.1013 +      moreover have "m' \<noteq> 0" using p by (intro notI) auto
  1.1014 +      ultimately have "m' \<noteq> 0 \<and>m' \<noteq> 1 \<and> m' \<noteq> 2" using that by auto
  1.1015 +      hence "m' > 2" by linarith
  1.1016 +  
  1.1017 +      show ?thesis
  1.1018 +      proof
  1.1019 +        assume "\<exists>g. residue_primroot m g"
  1.1020 +        with coprime p have coprime': "coprime (p - 1) (Carmichael m')"
  1.1021 +          using residue_primroot_modulus_mult_coprime_imp_Carmichael_coprime[OF coprime]
  1.1022 +          by (auto simp: Carmichael_prime_power)
  1.1023 +        moreover have "even (p - 1)" "even (Carmichael m')"
  1.1024 +          using \<open>m' > 2\<close> \<open>odd p\<close> by (auto intro!: even_Carmichael)
  1.1025 +        ultimately show False by force
  1.1026 +      qed
  1.1027 +    qed
  1.1028 +  qed auto
  1.1029 +
  1.1030 +  ultimately show ?thesis by metis
  1.1031 +qed
  1.1032 +
  1.1033 +lemma residue_primroot_is_generator:
  1.1034 +  assumes "m > 1" and "residue_primroot m g"
  1.1035 +  shows   "bij_betw (\<lambda>i. g ^ i mod m) {..<totient m} (totatives m)"
  1.1036 +  unfolding bij_betw_def
  1.1037 +proof
  1.1038 +  from assms have [simp]: "ord m g = totient m"
  1.1039 +    by (simp add: residue_primroot_def)
  1.1040 +  from assms have "coprime m g" by (simp add: residue_primroot_def)
  1.1041 +  hence "inj_on (\<lambda>i. g ^ i mod m) {..<ord m g}"
  1.1042 +    by (intro inj_power_mod)
  1.1043 +  thus inj: "inj_on (\<lambda>i. g ^ i mod m) {..<totient m}"
  1.1044 +    by simp
  1.1045 +
  1.1046 +  show "(\<lambda>i. g ^ i mod m) ` {..<totient m} = totatives m"
  1.1047 +  proof (rule card_subset_eq)
  1.1048 +    show "card ((\<lambda>i. g ^ i mod m) ` {..<totient m}) = card (totatives m)"
  1.1049 +      using inj by (subst card_image) (auto simp: totient_def)
  1.1050 +    show "(\<lambda>i. g ^ i mod m) ` {..<totient m} \<subseteq> totatives m"
  1.1051 +      using \<open>m > 1\<close> \<open>coprime m g\<close> power_in_totatives[of m g] by blast
  1.1052 +  qed auto
  1.1053 +qed
  1.1054 +
  1.1055 +text \<open>
  1.1056 +  Given one primitive root \<open>g\<close>, all the primitive roots are powers $g^i$ for
  1.1057 +  $1\leq i \leq \varphi(n)$ with $\text{gcd}(i, \varphi(n)) = 1$.
  1.1058 +\<close>
  1.1059 +theorem residue_primroot_bij_betw_primroots:
  1.1060 +  assumes "m > 1" and "residue_primroot m g"
  1.1061 +  shows   "bij_betw (\<lambda>i. g ^ i mod m) (totatives (totient m))
  1.1062 +                                      {g\<in>totatives m. residue_primroot m g}"
  1.1063 +proof (cases "m = 2")
  1.1064 +  case [simp]: True
  1.1065 +  have [simp]: "totatives 2 = {1}"
  1.1066 +    by (auto simp: totatives_def elim!: oddE)
  1.1067 +  from assms have "odd g"
  1.1068 +    by (auto simp: residue_primroot_def)
  1.1069 +  hence pow_eq: "(\<lambda>i. g ^ i mod m) = (\<lambda>_. 1)"
  1.1070 +    by (auto simp: fun_eq_iff mod_2_eq_odd)
  1.1071 +  have "{g \<in> totatives m. residue_primroot m g} = {1}"
  1.1072 +    by (auto simp: residue_primroot_def)
  1.1073 +  thus ?thesis using pow_eq by (auto simp: bij_betw_def)
  1.1074 +next
  1.1075 +  case False
  1.1076 +  thus ?thesis unfolding bij_betw_def
  1.1077 +  proof safe
  1.1078 +    from assms False have "m > 2" by auto
  1.1079 +    from assms \<open>m > 2\<close> have "totient m > 1" by (intro totient_gt_1) auto
  1.1080 +    from assms have [simp]: "ord m g = totient m"
  1.1081 +      by (simp add: residue_primroot_def)
  1.1082 +    from assms have "coprime m g" by (simp add: residue_primroot_def)
  1.1083 +    hence "inj_on (\<lambda>i. g ^ i mod m) {..<ord m g}"
  1.1084 +      by (intro inj_power_mod)
  1.1085 +    thus "inj_on (\<lambda>i. g ^ i mod m) (totatives (totient m))"
  1.1086 +      by (rule inj_on_subset)
  1.1087 +         (use assms \<open>totient m > 1\<close> in \<open>auto simp: totatives_less residue_primroot_def\<close>)
  1.1088 +
  1.1089 +    {
  1.1090 +      fix i assume i: "i \<in> totatives (totient m)"
  1.1091 +      from \<open>coprime m g\<close> and \<open>m > 2\<close> show "g ^ i mod m \<in> totatives m"
  1.1092 +        by (intro power_in_totatives) auto
  1.1093 +      show "residue_primroot m (g ^ i mod m)"
  1.1094 +        using i \<open>m > 2\<close> \<open>coprime m g\<close>
  1.1095 +        by (auto simp: residue_primroot_def coprime_commute ord_power totatives_def)
  1.1096 +    }
  1.1097 +    {
  1.1098 +      fix x assume x: "x \<in> totatives m" "residue_primroot m x"
  1.1099 +      then obtain i where i: "i < totient m" "x = (g ^ i mod m)"
  1.1100 +        using assms residue_primroot_is_generator[of m g] by (auto simp: bij_betw_def)
  1.1101 +      from i x \<open>m > 2\<close> have "i > 0" by (intro Nat.gr0I) (auto simp: residue_primroot_1_iff)
  1.1102 +      have "totient m div gcd i (totient m) = totient m"
  1.1103 +        using x i \<open>coprime m g\<close> by (auto simp add: residue_primroot_def ord_power)
  1.1104 +      hence "coprime i (totient m)"
  1.1105 +        unfolding coprime_iff_gcd_eq_1 using assms by (subst (asm) dvd_div_eq_mult) auto
  1.1106 +      with i \<open>i > 0\<close> have "i \<in> totatives (totient m)" by (auto simp: totatives_def)
  1.1107 +      thus "x \<in> (\<lambda>i. g ^ i mod m) ` totatives (totient m)" using i by auto
  1.1108 +    }
  1.1109 +  qed
  1.1110 +qed
  1.1111 +
  1.1112 +text \<open>
  1.1113 +  It follows from the above statement that any residue ring modulo \<open>n\<close> that \<^emph>\<open>has\<close> primitive roots
  1.1114 +  has exactly $\varphi(\varphi(n))$ of them.
  1.1115 +\<close>
  1.1116 +corollary card_residue_primroots:
  1.1117 +  assumes "\<exists>g. residue_primroot m g"
  1.1118 +  shows   "card {g\<in>totatives m. residue_primroot m g} = totient (totient m)"
  1.1119 +proof (cases "m = 1")
  1.1120 +  case [simp]: True
  1.1121 +  have "{g \<in> totatives m. residue_primroot m g} = {1}"
  1.1122 +    by (auto simp: residue_primroot_def)
  1.1123 +  thus ?thesis by simp
  1.1124 +next
  1.1125 +  case False
  1.1126 +  from assms obtain g where g: "residue_primroot m g" by auto
  1.1127 +  hence "m \<noteq> 0" by (intro notI) auto
  1.1128 +  with \<open>m \<noteq> 1\<close> have "m > 1" by linarith
  1.1129 +  from this g have "bij_betw (\<lambda>i. g ^ i mod m) (totatives (totient m))
  1.1130 +                      {g\<in>totatives m. residue_primroot m g}"
  1.1131 +    by (rule residue_primroot_bij_betw_primroots)
  1.1132 +  hence "card (totatives (totient m)) = card {g\<in>totatives m. residue_primroot m g}"
  1.1133 +    by (rule bij_betw_same_card)
  1.1134 +  thus ?thesis by (simp add: totient_def)
  1.1135 +qed
  1.1136 +
  1.1137 +corollary card_residue_primroots':
  1.1138 +  "card {g\<in>totatives m. residue_primroot m g} =
  1.1139 +     (if m \<in> cyclic_moduli then totient (totient m) else 0)"
  1.1140 +  by (simp add: residue_primroot_iff_in_cyclic_moduli [symmetric] card_residue_primroots)
  1.1141 +
  1.1142 +text \<open>
  1.1143 +  As an example, we evaluate $\lambda(122200)$ using the prime factorisation.
  1.1144 +\<close>
  1.1145 +lemma "Carmichael 122200 = 1380"
  1.1146 +proof -
  1.1147 +  have "prime_factorization (2^3 * 5^2 * 13 * 47) = {#2, 2, 2, 5, 5, 13, 47::nat#}"
  1.1148 +    by (intro prime_factorization_eqI) auto
  1.1149 +  from eval_Carmichael[OF this] show "Carmichael 122200 = 1380"
  1.1150 +    by (simp add: lcm_nat_def gcd_non_0_nat)
  1.1151 +qed
  1.1152 +
  1.1153 +(* TODO: definition of index ("discrete logarithm") *)
  1.1154 +
  1.1155 +end
  1.1156 \ No newline at end of file