src/HOL/Number_Theory/Residue_Primitive_Roots.thy

rule concerning bit (push_bit ...)

(*
  File:      HOL/Number_Theory/Residue_Primitive_Roots.thy
  Author:    Manuel Eberl

  Primitive roots in residue rings: Definition and existence criteria
*)
section \<open>Primitive roots in residue rings and Carmichael's function\<close>
theory Residue_Primitive_Roots
  imports Pocklington
begin

text \<open>
  This theory develops the notions of primitive roots (generators) in residue rings. It also
  provides a definition and all the basic properties of Carmichael's function $\lambda(n)$, which
  is strongly related to this. The proofs mostly follow Apostol's presentation
\<close>

subsection \<open>Primitive roots in residue rings\<close>

text \<open>
  A primitive root of a residue ring modulo \<open>n\<close> is an element \<open>g\<close> that \<^emph>\<open>generates\<close> the
  ring, i.\,e.\ such that for each \<open>x\<close> coprime to \<open>n\<close> there exists an \<open>i\<close> such that $x = g^i$.
  A simpler definition is that \<open>g\<close> must have the same order as the cardinality of the
  multiplicative group, which is $\varphi(n)$.

  Note that for convenience, this definition does \<^emph>\<open>not\<close> demand \<open>g < n\<close>.
\<close>
inductive residue_primroot :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
  "n > 0 \<Longrightarrow> coprime n g \<Longrightarrow> ord n g = totient n \<Longrightarrow> residue_primroot n g"

lemma residue_primroot_def [code]:
  "residue_primroot n x \<longleftrightarrow> n > 0 \<and> coprime n x \<and> ord n x = totient n"
  by (simp add: residue_primroot.simps)

lemma not_residue_primroot_0 [simp]: "~residue_primroot 0 x"
  by (auto simp: residue_primroot_def)

lemma residue_primroot_mod [simp]: "residue_primroot n (x mod n) = residue_primroot n x"
  by (cases "n = 0") (simp_all add: residue_primroot_def)

lemma residue_primroot_cong:
  assumes "[x = x'] (mod n)"
  shows   "residue_primroot n x = residue_primroot n x'"
proof -
  have "residue_primroot n x = residue_primroot n (x mod n)"
    by simp
  also have "x mod n = x' mod n"
    using assms by (simp add: cong_def)
  also have "residue_primroot n (x' mod n) = residue_primroot n x'"
    by simp
  finally show ?thesis .
qed

lemma not_residue_primroot_0_right [simp]: "residue_primroot n 0 \<longleftrightarrow> n = 1"
  by (auto simp: residue_primroot_def)

lemma residue_primroot_1_iff: "residue_primroot n (Suc 0) \<longleftrightarrow> n \<in> {1, 2}"
proof
  assume *: "residue_primroot n (Suc 0)"
  with totient_gt_1[of n] have "n \<le> 2" by (cases "n \<le> 2") (auto simp: residue_primroot_def)
  hence "n \<in> {0, 1, 2}" by auto
  thus "n \<in> {1, 2}" using * by (auto simp: residue_primroot_def)
qed (auto simp: residue_primroot_def)


subsection \<open>Primitive roots modulo a prime\<close>

text \<open>
  For prime \<open>p\<close>, we now analyse the number of elements in the ring $\mathbb{Z}/p\mathbb{Z}$
  whose order is precisely \<open>d\<close> for each \<open>d\<close>.
\<close>
context
  fixes n :: nat and \<psi>
  assumes n: "n > 1"
  defines "\<psi> \<equiv> (\<lambda>d. card {x\<in>totatives n. ord n x = d})"
begin

lemma elements_with_ord_restrict_totatives:
  "d > 0 \<Longrightarrow> {x\<in>{..<n}. ord n x = d} = {x\<in>totatives n. ord n x = d}"
  using n by (auto simp: totatives_def coprime_commute intro!: Nat.gr0I le_neq_trans)

lemma prime_elements_with_ord:
  assumes "\<psi> d \<noteq> 0" and "prime n"
      and a: "a \<in> totatives n" "ord n a = d" "a \<noteq> 1"
  shows   "inj_on (\<lambda>k. a ^ k mod n) {..<d}"
    and   "{x\<in>{..<n}. [x ^ d = 1] (mod n)} = (\<lambda>k. a ^ k mod n) ` {..<d}"
    and   "bij_betw (\<lambda>k. a ^ k mod n) (totatives d) {x\<in>{..<n}. ord n x = d}"
proof -
  show inj: "inj_on (\<lambda>k. a ^ k mod n) {..<d}"
    using inj_power_mod[of n a] a by (auto simp: totatives_def coprime_commute)
  from a have "d > 0" by (auto simp: totatives_def coprime_commute)
  moreover have "d \<noteq> 1" using a n
    by (auto simp: ord_eq_Suc_0_iff totatives_less cong_def)
  ultimately have d: "d > 1" by simp

  have *: "(\<lambda>k. a ^ k mod n) ` {..<d} = {x\<in>{..<n}. [x ^ d = 1] (mod n)}"
  proof (rule card_seteq)
    have "card {x\<in>{..<n}. [x ^ d = 1] (mod n)} \<le> d"
      using assms a by (intro roots_mod_prime_bound) (auto simp: totatives_def coprime_commute)
    also have "\<dots> = card ((\<lambda>k. a ^ k mod n) ` {..<d})"
      using inj by (subst card_image) auto
    finally show "card {x \<in> {..<n}. [x ^ d = 1] (mod n)} \<le> \<dots>" .
  next
    show "(\<lambda>k. a ^ k mod n) ` {..<d} \<subseteq> {x \<in> {..<n}. [x ^ d = 1] (mod n)}"
    proof safe
      fix k assume "k < d"
      have "[(a ^ d) ^ k = 1 ^ k] (mod n)"
        by (intro cong_pow) (use a in \<open>auto simp: ord_divides'\<close>)
      thus "[(a ^ k mod n) ^ d = 1] (mod n)"
        by (simp add: power_mult [symmetric] cong_def power_mod mult.commute)
    qed (use \<open>prime n\<close> in \<open>auto dest: prime_gt_1_nat\<close>)
  qed auto
  thus "{x\<in>{..<n}. [x ^ d = 1] (mod n)} = (\<lambda>k. a ^ k mod n) ` {..<d}" ..

  show "bij_betw (\<lambda>k. a ^ k mod n) (totatives d) {x\<in>{..<n}. ord n x = d}"
    unfolding bij_betw_def
  proof (intro conjI inj_on_subset[OF inj] equalityI subsetI)
    fix b assume "b \<in> (\<lambda>k. a ^ k mod n) ` totatives d"
    then obtain k where "b = a ^ k mod n" "k \<in> totatives d" by auto
    thus "b \<in> {b \<in> {..<n}. ord n b = d}"
      using n a by (simp add: ord_power totatives_def coprime_commute)
  next
    fix b assume "b \<in> {x \<in> {..<n}. ord n x = d}"
    hence b: "ord n b = d" "b < n" by auto
    with d have "coprime n b" using ord_eq_0[of n b] by auto
    from b have "b \<in> {x\<in>{..<n}. [x ^ d = 1] (mod n)}"
      by (auto simp: ord_divides')
    with * obtain k where k: "k < d" "b = a ^ k mod n"
      by blast
    with b(2) n a d have "d div gcd k d = ord n b"
      using \<open>coprime n b\<close> by (auto simp: ord_power)
    also have "ord n b = d" by (simp add: b)
    finally have "coprime k d"
      unfolding coprime_iff_gcd_eq_1 using d a by (subst (asm) div_eq_dividend_iff) auto
    with k b d have "k \<in> totatives d" by (auto simp: totatives_def intro!: Nat.gr0I)
    with k show "b \<in> (\<lambda>k. a ^ k mod n) ` totatives d" by blast
  qed (use d n in \<open>auto simp: totatives_less\<close>)
qed

lemma prime_card_elements_with_ord:
  assumes "\<psi> d \<noteq> 0" and "prime n"
  shows   "\<psi> d = totient d"
proof (cases "d = 1")
  case True
  have "\<psi> 1 = 1"
    using elements_with_ord_1[of n] n by (simp add: \<psi>_def)
  thus ?thesis using True by simp
next
  case False
  from assms obtain a where a: "a \<in> totatives n" "ord n a = d"
    by (auto simp: \<psi>_def)
  from a have "d > 0" by (auto intro!: Nat.gr0I simp: ord_eq_0 totatives_def coprime_commute)
  from a and False have "a \<noteq> 1" by auto
  from bij_betw_same_card[OF prime_elements_with_ord(3)[OF assms a this]] show "\<psi> d = totient d"
    using elements_with_ord_restrict_totatives[of d] False a \<open>d > 0\<close>
    by (simp add: \<psi>_def totient_def)
qed

lemma prime_sum_card_elements_with_ord_eq_totient:
  "(\<Sum>d | d dvd totient n. \<psi> d) = totient n"
proof -
  have "totient n = card (totatives n)"
    by (simp add: totient_def)
  also have "totatives n = (\<Union>d\<in>{d. d dvd totient n}. {x\<in>totatives n. ord n x = d})"
    by (force simp: order_divides_totient totatives_def coprime_commute)
  also have "card \<dots> = (\<Sum>d | d dvd totient n. \<psi> d)"
    unfolding \<psi>_def using n by (subst card_UN_disjoint) (auto intro!: finite_divisors_nat)
  finally show ?thesis ..
qed

text \<open>
  We can now show that the number of elements of order \<open>d\<close> is $\varphi(d)$ if $d\mid p - 1$
  and 0 otherwise.
\<close>
theorem prime_card_elements_with_ord_eq_totient:
  assumes "prime n"
  shows   "\<psi> d = (if d dvd n - 1 then totient d else 0)"
proof (cases "d dvd totient n")
  case False
  thus ?thesis using order_divides_totient[of n] assms
    by (auto simp: \<psi>_def totient_prime totatives_def coprime_commute[of n])
next
  case True
  have "\<psi> d = totient d"
  proof (rule ccontr)
    assume neq: "\<psi> d \<noteq> totient d"
    have le: "\<psi> d \<le> totient d" if "d dvd totient n" for d
      using prime_card_elements_with_ord[of d] assms by (cases "\<psi> d = 0") auto
    from neq and le[of d] and True have less: "\<psi> d < totient d" by auto
  
    have "totient n = (\<Sum>d | d dvd totient n. \<psi> d)"
      using prime_sum_card_elements_with_ord_eq_totient ..
    also have "\<dots> < (\<Sum>d | d dvd totient n. totient d)"
      by (rule sum_strict_mono_ex1)
         (use n le less assms True in \<open>auto intro!: finite_divisors_nat\<close>)
    also have "\<dots> = totient n"
      using totient_divisor_sum .
    finally show False by simp
  qed
  with True show ?thesis using assms by (simp add: totient_prime)
qed

text \<open>
  As a corollary, we get that the number of primitive roots modulo a prime \<open>p\<close> is
  $\varphi(p - 1)$. Since this number is positive, we also get that there \<^emph>\<open>is\<close> at least
  one primitive root modulo \<open>p\<close>.
\<close>
lemma
  assumes "prime n"
  shows   prime_card_primitive_roots:  "card {x\<in>totatives n. ord n x = n - 1} = totient (n - 1)"
                                       "card {x\<in>{..<n}. ord n x = n - 1} = totient (n - 1)"
  and     prime_primitive_root_exists: "\<exists>x. residue_primroot n x"
proof -
  show *: "card {x\<in>totatives n. ord n x = n - 1} = totient (n - 1)"
    using prime_card_elements_with_ord_eq_totient[of "n - 1"] assms
    by (auto simp: totient_prime \<psi>_def)
  thus "card {x\<in>{..<n}. ord n x = n - 1} = totient (n - 1)"
    using assms n elements_with_ord_restrict_totatives[of "n - 1"] by simp
  
  note *
  also have "totient (n - 1) > 0" using n by auto
  finally show "\<exists>x. residue_primroot n x" using assms prime_gt_1_nat[of n]
    by (subst (asm) card_gt_0_iff)
       (auto simp: residue_primroot_def totient_prime totatives_def coprime_commute)
qed

end


subsection \<open>Primitive roots modulo powers of an odd prime\<close>

text \<open>
  Any primitive root \<open>g\<close> modulo an odd prime \<open>p\<close> is also a primitive root modulo $p^k$ for all
  $k > 0$ if $[g^{p - 1} \neq 1]\ (\text{mod}\ p^2)$. To show this, we first need the
  following lemma.
\<close>
lemma residue_primroot_power_prime_power_neq_1:
  assumes "k \<ge> 2"
  assumes p: "prime p" "odd p" and "residue_primroot p g" and "[g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
  shows   "[g ^ totient (p ^ (k - 1)) \<noteq> 1] (mod (p ^ k))"
  using assms(1)
proof (induction k rule: dec_induct)
  case base
  thus ?case using assms by (simp add: totient_prime)
next
  case (step k)
  from p have "p > 2"
    using prime_gt_1_nat[of p] by (cases "p = 2") auto
  from assms have g: "g > 0" by (auto intro!: Nat.gr0I)
  have "[g ^ totient (p ^ (k - 1)) = 1] (mod p ^ (k - 1))"
    using assms by (intro euler_theorem)
                   (auto simp: residue_primroot_def totatives_def coprime_commute)
  from cong_to_1_nat[OF this]
    obtain t where *: "g ^ totient (p ^ (k - 1)) - 1 = p ^ (k - 1) * t" by auto
  have t: "g ^ totient (p ^ (k - 1)) = p ^ (k - 1) * t + 1"
    using g by (subst * [symmetric]) auto 

  have "\<not>p dvd t"
  proof
    assume "p dvd t"
    then obtain q where [simp]: "t = p * q" by auto
    from t have "g ^ totient (p ^ (k - 1)) = p ^ k * q + 1"
      using \<open>k \<ge> 2\<close> by (cases k) auto
    hence "[g ^ totient (p ^ (k - 1)) = p ^ k * q + 1] (mod p ^ k)"
      by simp
    also have "[p ^ k * q + 1 = 0 * q + 1] (mod p ^ k)"
      by (intro cong_add cong_mult) (auto simp: cong_0_iff)
    finally have "[g ^ totient (p ^ (k - 1)) = 1] (mod p ^ k)"
      by simp
    with step.IH show False by contradiction
  qed

  from t have "(g ^ totient (p ^ (k - 1))) ^ p = (p ^ (k - 1) * t + 1) ^ p"
    by (rule arg_cong)
  also have "(g ^ totient (p ^ (k - 1))) ^ p = g ^ (p * totient (p ^ (k - 1)))"
    by (simp add: power_mult [symmetric] mult.commute)
  also have "p * totient (p ^ (k - 1)) = totient (p ^ k)"
    using p \<open>k \<ge> 2\<close> by (simp add: totient_prime_power Suc_diff_Suc flip: power_Suc)
  also have "(p ^ (k - 1) * t + 1) ^ p = (\<Sum>i\<le>p. (p choose i) * t ^ i * p ^ (i * (k - 1)))"
    by (subst binomial) (simp_all add: mult_ac power_mult_distrib power_mult [symmetric])
  finally have "[g ^ totient (p ^ k) = (\<Sum>i\<le>p. (p choose i) * t ^ i * p ^ (i * (k - 1)))]
                  (mod (p ^ Suc k))" (is "[_ = ?rhs] (mod _)") by simp

  also have "[?rhs = (\<Sum>i\<le>p. if i \<le> 1 then (p choose i) * t ^ i * p ^ (i * (k - 1)) else 0)]
               (mod (p ^ Suc k))" (is "[sum ?f _ = sum ?g _] (mod _)")
  proof (intro cong_sum)
    fix i assume i: "i \<in> {..p}"
    consider "i \<le> 1" | "i = 2" | "i > 2" by force
    thus "[?f i = ?g i] (mod (p ^ Suc k))"
    proof cases
      assume i: "i > 2"
      have "Suc k \<le> 3 * (k - 1)"
        using \<open>k \<ge> 2\<close> by (simp add: algebra_simps)
      also have "3 * (k - 1) \<le> i * (k - 1)"
        using i by (intro mult_right_mono) auto
      finally have "p ^ Suc k dvd ?f i"
        by (intro dvd_mult le_imp_power_dvd)
      thus "[?f i = ?g i] (mod (p ^ Suc k))"
        by (simp add: cong_0_iff)
    next
      assume [simp]: "i = 2"
      have "?f i = p * (p - 1) div 2 * t\<^sup>2 * p ^ (2 * (k - 1))"
        using choose_two[of p] by simp
      also have "p * (p - 1) div 2 = (p - 1) div 2 * p"
        using \<open>odd p\<close> by (auto elim!: oddE)
      also have "\<dots> * t\<^sup>2 * p ^ (2 * (k - 1)) = (p - 1) div 2 * t\<^sup>2 * (p * p ^ (2 * (k - 1)))"
        by (simp add: algebra_simps)
      also have "p * p ^ (2 * (k - 1)) = p ^ (2 * k - 1)"
        using \<open>k \<ge> 2\<close> by (cases k) auto
      also have "p ^ Suc k dvd (p - 1) div 2 * t\<^sup>2 * p ^ (2 * k - 1)"
        using \<open>k \<ge> 2\<close> by (intro dvd_mult le_imp_power_dvd) auto
      finally show "[?f i = ?g i] (mod (p ^ Suc k))"
        by (simp add: cong_0_iff)
    qed auto
  qed
  also have "(\<Sum>i\<le>p. ?g i) = (\<Sum>i\<le>1. ?f i)"
    using p prime_gt_1_nat[of p] by (intro sum.mono_neutral_cong_right) auto
  also have "\<dots> = 1 + t * p ^ k"
    using choose_two[of p] \<open>k \<ge> 2\<close> by (cases k) simp_all
  finally have eq: "[g ^ totient (p ^ k) = 1 + t * p ^ k] (mod p ^ Suc k)" .

  have "[g ^ totient (p ^ k) \<noteq> 1] (mod p ^ Suc k)"
  proof
    assume "[g ^ totient (p ^ k) = 1] (mod p ^ Suc k)"
    hence "[g ^ totient (p ^ k) - g ^ totient (p ^ k) = 1 + t * p ^ k - 1] (mod p ^ Suc k)"
      by (intro cong_diff_nat eq) auto
    hence "[t * p ^ k = 0] (mod p ^ Suc k)"
      by (simp add: cong_sym_eq)
    hence "p * p ^ k dvd t * p ^ k"
      by (simp add: cong_0_iff)
    hence "p dvd t" using \<open>p > 2\<close> by simp
    with \<open>\<not>p dvd t\<close> show False by contradiction
  qed
  thus ?case by simp
qed

text \<open>
  We can now show that primitive roots modulo \<open>p\<close> with the above condition are
  indeed also primitive roots modulo $p^k$.
\<close>
proposition residue_primroot_prime_lift_iff:
  assumes p: "prime p" "odd p" and "residue_primroot p g"
  shows   "(\<forall>k>0. residue_primroot (p ^ k) g) \<longleftrightarrow> [g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
proof -
  from assms have g: "coprime p g" "ord p g = p - 1"
    by (auto simp: residue_primroot_def totient_prime)
  show ?thesis
  proof
    assume "\<forall>k>0. residue_primroot (p ^ k) g"
    hence "residue_primroot (p\<^sup>2) g" by auto
    hence "ord (p\<^sup>2) g = totient (p\<^sup>2)"
      by (simp_all add: residue_primroot_def)
    thus "[g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
      using g assms prime_gt_1_nat[of p]
      by (auto simp: ord_divides' totient_prime_power)
  next
    assume g': "[g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"

    have "residue_primroot (p ^ k) g" if "k > 0" for k
    proof (cases "k = 1")
      case False
      with that have k: "k > 1" by simp
      from g have coprime: "coprime (p ^ k) g"
        by (auto simp: totatives_def coprime_commute)

      define t where "t = ord (p ^ k) g"
      have "[g ^ t = 1] (mod (p ^ k))"
        by (simp add: t_def ord_divides')
      also have "p ^ k = p * p ^ (k - 1)"
        using k by (cases k) auto
      finally have "[g ^ t = 1] (mod p)"
        by (rule cong_modulus_mult_nat)
      hence "totient p dvd t"
        using g p by (simp add: ord_divides' totient_prime)
      then obtain q where t: "t = totient p * q" by auto

      have "t dvd totient (p ^ k)"
        using coprime by (simp add: t_def order_divides_totient)
      with t p k have "q dvd p ^ (k - 1)" using prime_gt_1_nat[of p]
        by (auto simp: totient_prime totient_prime_power)
      then obtain b where b: "b \<le> k - 1" "q = p ^ b"
        using divides_primepow_nat[of p q "k - 1"] p by auto

      have "b = k - 1"
      proof (rule ccontr)
        assume "b \<noteq> k - 1"
        with b have "b < k - 1" by simp
        have "t = p ^ b * (p - 1)"
          using b p by (simp add: t totient_prime)
        also have "\<dots> dvd p ^ (k - 2) * (p - 1)"
          using \<open>b < k - 1\<close> by (intro mult_dvd_mono le_imp_power_dvd) auto
        also have "\<dots> = totient (p ^ (k - 1))"
          using k p by (simp add: totient_prime_power numeral_2_eq_2)
        finally have "[g ^ totient (p ^ (k - 1)) = 1] (mod (p ^ k))"
          by (simp add: ord_divides' t_def)
        with residue_primroot_power_prime_power_neq_1[of k p g] p k assms g' show False
          by auto
      qed
      hence "t = totient (p ^ k)"
        using p k by (simp add: t b totient_prime totient_prime_power)
      thus "residue_primroot (p ^ k) g"
        using g one_less_power[of p k] prime_gt_1_nat[of p] p k
        by (simp add: residue_primroot_def t_def)
    qed (use assms in auto)
    thus "\<forall>k>0. residue_primroot (p ^ k) g" by blast
  qed
qed

text \<open>
  If \<open>p\<close> is an odd prime, there is always a primitive root \<open>g\<close> modulo \<open>p\<close>, and if \<open>g\<close> does not
  fulfil the above assumption required for it to be liftable to $p^k$, we can use $g + p$, which
  is also a primitive root modulo \<open>p\<close> and \<^emph>\<open>does\<close> fulfil the assumption.

  This shows that any modulus that is a power of an odd prime has a primitive root.
\<close>
theorem residue_primroot_odd_prime_power_exists:
  assumes p: "prime p" "odd p"
  obtains g where "\<forall>k>0. residue_primroot (p ^ k) g"
proof -
  obtain g where g: "residue_primroot p g"
    using prime_primitive_root_exists[of p] assms prime_gt_1_nat[of p] by auto

  have "\<exists>g. residue_primroot p g \<and> [g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
  proof (cases "[g ^ (p - 1) = 1] (mod p\<^sup>2)")
    case True
    define g' where "g' = p + g"
    note g
    also have "residue_primroot p g \<longleftrightarrow> residue_primroot p g'"
      unfolding g'_def by (rule residue_primroot_cong) (auto simp: cong_def)
    finally have g': "residue_primroot p g'" .

    have "[g' ^ (p - 1) = (\<Sum>k\<le>p-1. ((p-1) choose k) * g ^ (p - Suc k) * p ^ k)] (mod p\<^sup>2)"
      (is "[_ = ?rhs] (mod _)") by (simp add: g'_def binomial mult_ac)
    also have "[?rhs = (\<Sum>k\<le>p-1. if k \<le> 1 then ((p-1) choose k) *
                                   g ^ (p - Suc k) * p ^ k else 0)] (mod p\<^sup>2)"
      (is "[sum ?f _ = sum ?g _] (mod _)")
    proof (intro cong_sum)
      fix k assume "k \<in> {..p-1}"
      show "[?f k = ?g k] (mod p\<^sup>2)"
      proof (cases "k \<le> 1")
        case False
        have "p\<^sup>2 dvd ?f k"
          using False by (intro dvd_mult le_imp_power_dvd) auto
        thus ?thesis using False by (simp add: cong_0_iff)
      qed auto
    qed
    also have "sum ?g {..p-1} = sum ?f {0, 1}"
      using prime_gt_1_nat[of p] p by (intro sum.mono_neutral_cong_right) auto
    also have "\<dots> = g ^ (p - 1) + p * (p - 1) * g ^ (p - 2)"
      using p by (simp add: numeral_2_eq_2)
    also have "[g ^ (p - 1) + p * (p - 1) * g ^ (p - 2) = 1 + p * (p - 1) * g ^ (p - 2)] (mod p\<^sup>2)"
      by (intro cong_add True) auto
    finally have "[g' ^ (p - 1) = 1 + p * (p - 1) * g ^ (p - 2)] (mod p\<^sup>2)" .

    moreover have "[1 + p * (p - 1) * g ^ (p - 2) \<noteq> 1] (mod p\<^sup>2)"
    proof
      assume "[1 + p * (p - 1) * g ^ (p - 2) = 1] (mod p\<^sup>2)"
      hence "[1 + p * (p - 1) * g ^ (p - 2) - 1 = 1 - 1] (mod p\<^sup>2)"
        by (intro cong_diff_nat) auto
      hence "p * p dvd p * ((p - 1) * g ^ (p - 2))"
        by (auto simp: cong_0_iff power2_eq_square)
      hence "p dvd (p - 1) * g ^ (p - 2)"
        using p by simp
      hence "p dvd g ^ (p - 2)"
        using p dvd_imp_le[of p "p - Suc 0"] prime_gt_1_nat[of p]
        by (auto simp: prime_dvd_mult_iff)
      also have "\<dots> dvd g ^ (p - 1)"
        by (intro le_imp_power_dvd) auto
      finally have "[g ^ (p - 1) = 0] (mod p)"
        by (simp add: cong_0_iff)
      hence "[0 = g ^ (p - 1)] (mod p)"
        by (simp add: cong_sym_eq)

      also from \<open>residue_primroot p g\<close> have "[g ^ (p - 1) = 1] (mod p)"
        using p by (auto simp: residue_primroot_def ord_divides' totient_prime)
      finally have "[0 = 1] (mod p)" .
      thus False using prime_gt_1_nat[of p] p by (simp add: cong_def)
    qed

    ultimately have "[g' ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
      by (simp add: cong_def)
    thus "\<exists>g. residue_primroot p g \<and> [g ^ (p - 1) \<noteq> 1] (mod p\<^sup>2)"
      using g' by blast    
  qed (use g in auto)
  thus ?thesis
    using residue_primroot_prime_lift_iff[OF assms] that by blast
qed


subsection \<open>Carmichael's function\<close>

text \<open>
  Carmichael's function $\lambda(n)$ gives the LCM of the orders of all elements in the
  residue ring modulo $n$ -- or, equivalently, the maximum order, as we will show later.
  Algebraically speaking, it is the exponent of the multiplicative group
  $(\mathbb{Z}/n\mathbb{Z})^*$.

  It is not to be confused with Liouville's function, which is also denoted by $\lambda(n)$.
\<close>
definition Carmichael where
  "Carmichael n = (LCM a \<in> totatives n. ord n a)"

lemma Carmichael_0 [simp]: "Carmichael 0 = 1"
  by (simp add: Carmichael_def)

lemma Carmichael_1 [simp]: "Carmichael 1 = 1"
  by (simp add: Carmichael_def)

lemma Carmichael_Suc_0 [simp]: "Carmichael (Suc 0) = 1"
  by (simp add: Carmichael_def)

lemma ord_dvd_Carmichael:
  assumes "n > 1" "coprime n k"
  shows   "ord n k dvd Carmichael n"
proof -
  have "k mod n \<in> totatives n"
    using assms by (auto simp: totatives_def coprime_commute intro!: Nat.gr0I)
  hence "ord n (k mod n) dvd Carmichael n"
    by (simp add: Carmichael_def del: ord_mod)
  thus ?thesis by simp
qed

lemma Carmichael_divides:
  assumes "Carmichael n dvd k" "coprime n a"
  shows   "[a ^ k = 1] (mod n)"
proof (cases "n < 2 \<or> a = 1")
  case False
  hence "ord n a dvd Carmichael n"
    using False assms by (intro ord_dvd_Carmichael) auto
  also have "\<dots> dvd k" by fact
  finally have "ord n a dvd k" .
  thus ?thesis using ord_divides by auto
next
  case True
  then consider "a = 1" | "n = 0" | "n = 1" by force
  thus ?thesis using assms by cases auto
qed

lemma Carmichael_dvd_totient: "Carmichael n dvd totient n"
  unfolding Carmichael_def
proof (intro Lcm_least, safe)
  fix a assume "a \<in> totatives n"
  hence "[a ^ totient n = 1] (mod n)"
    by (intro euler_theorem) (auto simp: totatives_def)
  thus "ord n a dvd totient n"
    using ord_divides by blast
qed

lemma Carmichael_dvd_mono_coprime:
  assumes "coprime m n" "m > 1" "n > 1"
  shows   "Carmichael m dvd Carmichael (m * n)"
  unfolding Carmichael_def[of m]
proof (intro Lcm_least, safe)
  fix x assume x: "x \<in> totatives m"
  from assms have "totatives n \<noteq> {}" by simp
  then obtain y where y: "y \<in> totatives n" by blast

  from binary_chinese_remainder_nat[OF assms(1), of x y]
  obtain z where z: "[z = x] (mod m)" "[z = y] (mod n)" by blast
  have z': "coprime z n" "coprime z m"
    by (rule cong_imp_coprime; use x y z in \<open>force simp: totatives_def cong_sym_eq\<close>)+

  from z have "ord m x = ord m z"
    by (intro ord_cong) (auto simp: cong_sym_eq)
  also have "ord m z dvd ord (m * n) z"
    using assms by (auto simp: ord_modulus_mult_coprime)
  also from z' assms have "\<dots> dvd Carmichael (m * n)"
    by (intro ord_dvd_Carmichael) (auto simp: coprime_commute intro!:one_less_mult)
  finally show "ord m x dvd Carmichael (m * n)" .
qed

text \<open>
  $\lambda$ distributes over the product of coprime numbers similarly to $\varphi$, but
  with LCM instead of multiplication:
\<close>
lemma Carmichael_mult_coprime:
  assumes "coprime m n"
  shows   "Carmichael (m * n) = lcm (Carmichael m) (Carmichael n)"
proof (cases "m \<le> 1 \<or> n \<le> 1")
  case True
  hence "m = 0 \<or> n = 0 \<or> m = 1 \<or> n = 1" by force
  thus ?thesis using assms by auto
next
  case False
  show ?thesis
  proof (rule dvd_antisym)
    show "Carmichael (m * n) dvd lcm (Carmichael m) (Carmichael n)"
      unfolding Carmichael_def[of "m * n"]
    proof (intro Lcm_least, safe)
      fix x assume x: "x \<in> totatives (m * n)"
      have "ord (m * n) x = lcm (ord m x) (ord n x)"
        using assms x by (subst ord_modulus_mult_coprime) (auto simp: coprime_commute totatives_def)
      also have "\<dots> dvd lcm (Carmichael m) (Carmichael n)"
        using False x
        by (intro lcm_mono ord_dvd_Carmichael) (auto simp: totatives_def coprime_commute)
      finally show "ord (m * n) x dvd \<dots>" .
    qed
  next
    show "lcm (Carmichael m) (Carmichael n) dvd Carmichael (m * n)"
      using Carmichael_dvd_mono_coprime[of m n]
            Carmichael_dvd_mono_coprime[of n m] assms False
      by (auto intro!: lcm_least simp: coprime_commute mult.commute)
  qed
qed

lemma Carmichael_pos [simp, intro]: "Carmichael n > 0"
  by (auto simp: Carmichael_def ord_eq_0 totatives_def coprime_commute intro!: Nat.gr0I)

lemma Carmichael_nonzero [simp]: "Carmichael n \<noteq> 0"
  by simp

lemma power_Carmichael_eq_1:
  assumes "n > 1" "coprime n x"
  shows   "[x ^ Carmichael n = 1] (mod n)"
  using ord_dvd_Carmichael[of n x] assms
  by (auto simp: ord_divides')

lemma Carmichael_2 [simp]: "Carmichael 2 = 1"
  using Carmichael_dvd_totient[of 2] by simp

lemma Carmichael_4 [simp]: "Carmichael 4 = 2"
proof -
  have "Carmichael 4 dvd 2"
    using Carmichael_dvd_totient[of 4] by simp
  hence "Carmichael 4 \<le> 2" by (rule dvd_imp_le) auto
  moreover have "Carmichael 4 \<noteq> 1"
    using power_Carmichael_eq_1[of "4::nat" 3]
    unfolding coprime_iff_gcd_eq_1 by (auto simp: gcd_non_0_nat cong_def)
  ultimately show ?thesis
    using Carmichael_pos[of 4] by linarith
qed

lemma residue_primroot_Carmichael:
  assumes "residue_primroot n g"
  shows   "Carmichael n = totient n"
proof (cases "n = 1")
  case False
  show ?thesis
  proof (intro dvd_antisym Carmichael_dvd_totient)
    have "ord n g dvd Carmichael n"
      using assms False by (intro ord_dvd_Carmichael) (auto simp: residue_primroot_def)
    thus "totient n dvd Carmichael n"
      using assms by (auto simp: residue_primroot_def)
  qed
qed auto

lemma Carmichael_odd_prime_power:
  assumes "prime p" "odd p" "k > 0"
  shows   "Carmichael (p ^ k) = p ^ (k - 1) * (p - 1)"
proof -
  from assms obtain g where "residue_primroot (p ^ k) g"
    using residue_primroot_odd_prime_power_exists[of p] assms by metis
  hence "Carmichael (p ^ k) = totient (p ^ k)"
    by (intro residue_primroot_Carmichael[of "p ^ k" g]) auto
  with assms show ?thesis by (simp add: totient_prime_power)
qed

lemma Carmichael_prime:
  assumes "prime p"
  shows   "Carmichael p = p - 1"
proof (cases "even p")
  case True
  with assms have "p = 2"
    using primes_dvd_imp_eq two_is_prime_nat by blast
  thus ?thesis by simp
next
  case False
  with Carmichael_odd_prime_power[of p 1] assms show ?thesis by simp
qed
  
lemma Carmichael_twopow_ge_8:
  assumes "k \<ge> 3"
  shows   "Carmichael (2 ^ k) = 2 ^ (k - 2)"
proof (intro dvd_antisym)
  have "2 ^ (k - 2) = ord (2 ^ k) (3 :: nat)"
    using ord_twopow_3_5[of k 3] assms by simp
  also have "\<dots> dvd Carmichael (2 ^ k)"
    using assms one_less_power[of "2::nat" k] by (intro ord_dvd_Carmichael) auto
  finally show "2 ^ (k - 2) dvd \<dots>" .
next
  show "Carmichael (2 ^ k) dvd 2 ^ (k - 2)"
    unfolding Carmichael_def
  proof (intro Lcm_least, safe)
    fix x assume "x \<in> totatives (2 ^ k)"
    hence "odd x" by (auto simp: totatives_def)
    hence "[x ^ 2 ^ (k - 2) = 1] (mod 2 ^ k)"
      using assms ord_twopow_aux[of k x] by auto
    thus "ord (2 ^ k) x dvd 2 ^ (k - 2)"
      by (simp add: ord_divides')
  qed
qed

lemma Carmichael_twopow:
  "Carmichael (2 ^ k) = (if k \<le> 2 then 2 ^ (k - 1) else 2 ^ (k - 2))"
proof -
  have "k = 0 \<or> k = 1 \<or> k = 2 \<or> k \<ge> 3" by linarith
  thus ?thesis by (auto simp: Carmichael_twopow_ge_8)
qed

lemma Carmichael_prime_power:
  assumes "prime p" "k > 0"
  shows   "Carmichael (p ^ k) =
             (if p = 2 \<and> k > 2 then 2 ^ (k - 2) else p ^ (k - 1) * (p - 1))"
proof (cases "p = 2")
  case True
  thus ?thesis by (simp add: Carmichael_twopow)
next
  case False
  with assms have "odd p" "p > 2"
    using prime_odd_nat[of p] prime_gt_1_nat[of p] by auto
  thus ?thesis
    using assms Carmichael_odd_prime_power[of p k] by simp
qed

lemma Carmichael_prod_coprime:
  assumes "finite A" "\<And>i j. i \<in> A \<Longrightarrow> j \<in> A \<Longrightarrow> i \<noteq> j \<Longrightarrow> coprime (f i) (f j)"
  shows   "Carmichael (\<Prod>i\<in>A. f i) = (LCM i\<in>A. Carmichael (f i))"
  using assms by (induction A rule: finite_induct)
                 (simp, simp, subst Carmichael_mult_coprime[OF prod_coprime_right], auto)

text \<open>
  Since $\lambda$ distributes over coprime factors and we know the value of $\lambda(p^k)$
  for prime $p$, we can now give a closed formula for $\lambda(n)$ in terms of the prime
  factorisation of $n$:
\<close>
theorem Carmichael_closed_formula:
  "Carmichael n =
     (LCM p\<in>prime_factors n. let k = multiplicity p n
                             in  if p = 2 \<and> k > 2 then 2 ^ (k - 2) else p ^ (k - 1) * (p - 1))"
  (is "_ = Lcm ?A")
proof (cases "n = 0")
  case False
  hence "n = (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n)"
    using prime_factorization_nat by blast
  also have "Carmichael \<dots> =
               (LCM p\<in>prime_factors n. Carmichael (p ^ multiplicity p n))"
    by (subst Carmichael_prod_coprime) (auto simp: in_prime_factors_iff primes_coprime)
  also have "(\<lambda>p. Carmichael (p ^ multiplicity p n)) ` prime_factors n = ?A"
    by (intro image_cong)
       (auto simp: Let_def Carmichael_prime_power prime_factors_multiplicity)
  finally show ?thesis .
qed auto

corollary even_Carmichael:
  assumes "n > 2"
  shows   "even (Carmichael n)"
proof (cases "\<exists>k. n = 2 ^ k")
  case True
  then obtain k where [simp]: "n = 2 ^ k" by auto
  from assms have "k \<noteq> 0" "k \<noteq> 1" by (auto intro!: Nat.gr0I)
  hence "k \<ge> 2" by auto
  thus ?thesis by (auto simp: Carmichael_twopow)
next
  case False
  from assms have "n \<noteq> 0" by auto
  from False have "\<exists>p\<in>prime_factors n. p \<noteq> 2"
    using assms Ex_other_prime_factor[of n 2] by auto
  from divide_out_primepow_ex[OF \<open>n \<noteq> 0\<close> this] guess p k n' . note p = this
  from p have coprime: "coprime (p ^ k) n'"
    using p prime_imp_coprime by auto
  have "odd p"
    using p primes_dvd_imp_eq[of 2 p] by auto
  have "even (Carmichael (p ^ k))"
    using p \<open>odd p\<close> by (auto simp: Carmichael_prime_power)
  with p coprime show ?thesis
    by (auto simp: Carmichael_mult_coprime intro!: dvd_lcmI1)
qed

lemma eval_Carmichael:
  assumes "prime_factorization n = A"
  shows     "Carmichael n = (LCM p \<in> set_mset A.
               let k = count A p in if p = 2 \<and> k > 2 then 2 ^ (k - 2) else p ^ (k - 1) * (p - 1))"
  unfolding assms [symmetric] Carmichael_closed_formula
  by (intro arg_cong[where f = Lcm] image_cong) (auto simp: Let_def count_prime_factorization)

text \<open>
  Any residue ring always contains a $\lambda$-root, i.\,e.\ an element whose
  order is $\lambda(n)$.
\<close>
theorem Carmichael_root_exists:
  assumes "n > (0::nat)"
  obtains g where "g \<in> totatives n" and "ord n g = Carmichael n"
proof (cases "n = 1")
  case True
  thus ?thesis by (intro that[of 1]) (auto simp: totatives_def)
next
  case False
  have primepow: "\<exists>g. coprime (p ^ k) g \<and> ord (p ^ k) g = Carmichael (p ^ k)"
    if pk: "prime p" "k > 0" for p k
  proof (cases "p = 2")
    case [simp]: True
    from \<open>k > 0\<close> consider "k = 1" | "k = 2" | "k \<ge> 3" by force
    thus ?thesis
    proof cases
      assume "k = 1"
      thus ?thesis by (intro exI[of _ 1]) auto
    next
      assume [simp]: "k = 2"
      have "coprime 4 (3::nat)"
        by (auto simp: coprime_iff_gcd_eq_1 gcd_non_0_nat)
      thus ?thesis by (intro exI[of _ 3]) auto
    next
      assume k: "k \<ge> 3"
      have "coprime (2 ^ k :: nat) 3" by auto
      thus ?thesis using k
        by (intro exI[of _ 3]) (auto simp: ord_twopow_3_5 Carmichael_twopow)
    qed
  next
    case False
    hence "odd p" using \<open>prime p\<close>
      using primes_dvd_imp_eq two_is_prime_nat by blast
    then obtain g where "residue_primroot (p ^ k) g"
      using residue_primroot_odd_prime_power_exists[of p] pk by metis
    thus ?thesis using False pk
      by (intro exI[of _ g])
         (auto simp: Carmichael_prime_power residue_primroot_def totient_prime_power)
  qed

  define P where "P = prime_factors n"
  define k where "k = (\<lambda>p. multiplicity p n)"
  have "\<forall>p\<in>P. \<exists>g. coprime (p ^ k p) g \<and> ord (p ^ k p) g = Carmichael (p ^ k p)"
    using primepow by (auto simp: P_def k_def prime_factors_multiplicity)
  hence "\<exists>g. \<forall>p\<in>P. coprime (p ^ k p) (g p) \<and> ord (p ^ k p) (g p) = Carmichael (p ^ k p)"
    by (subst (asm) bchoice_iff)
  then obtain g where g: "\<And>p. p \<in> P \<Longrightarrow> coprime (p ^ k p) (g p)"
                         "\<And>p. p \<in> P \<Longrightarrow> ord (p ^ k p) (g p) = Carmichael (p ^ k p)" by metis
  have "\<exists>x. \<forall>i\<in>P. [x = g i] (mod i ^ k i)"
    by (intro chinese_remainder_nat)
       (auto simp: P_def k_def in_prime_factors_iff primes_coprime)
  then obtain x where x: "\<And>p. p \<in> P \<Longrightarrow> [x = g p] (mod p ^ k p)" by metis

  have "n = (\<Prod>p\<in>P. p ^ k p)"
    using assms unfolding P_def k_def by (rule prime_factorization_nat)
  also have "ord \<dots> x = (LCM p\<in>P. ord (p ^ k p) x)"
    by (intro ord_modulus_prod_coprime) (auto simp: P_def in_prime_factors_iff primes_coprime)
  also have "(\<lambda>p. ord (p ^ k p) x) ` P = (\<lambda>p. ord (p ^ k p) (g p)) ` P"
    by (intro image_cong ord_cong x) auto
  also have "\<dots> = (\<lambda>p. Carmichael (p ^ k p)) ` P"
    by (intro image_cong g) auto
  also have "Lcm \<dots> = Carmichael (\<Prod>p\<in>P. p ^ k p)"
    by (intro Carmichael_prod_coprime [symmetric])
       (auto simp: P_def in_prime_factors_iff primes_coprime)
  also have "(\<Prod>p\<in>P. p ^ k p) = n"
    using assms unfolding P_def k_def by (rule prime_factorization_nat [symmetric])
  finally have "ord n x = Carmichael n" .
  moreover from this have "coprime n x"
    by (cases "coprime n x") (auto split: if_splits)
  ultimately show ?thesis using assms False
    by (intro that[of "x mod n"])
       (auto simp: totatives_def coprime_commute coprime_absorb_left intro!: Nat.gr0I)
qed

text \<open>
  This also means that the Carmichael number is not only the LCM of the orders
  of the elements of the residue ring, but indeed the maximum of the orders.
\<close>
lemma Carmichael_altdef:
  "Carmichael n = (if n = 0 then 1 else Max (ord n ` totatives n))"
proof (cases "n = 0")
  case False
  have "Carmichael n = Max (ord n ` totatives n)"
  proof (intro antisym Max.boundedI Max.coboundedI)
    fix k assume k: "k \<in> ord n ` totatives n"
    thus "k \<le> Carmichael n"
    proof (cases "n = 1")
      case False
      with \<open>n \<noteq> 0\<close> have "n > 1" by linarith
      thus ?thesis using k \<open>n \<noteq> 0\<close>
        by (intro dvd_imp_le)
           (auto intro!: ord_dvd_Carmichael simp: totatives_def coprime_commute)
    qed auto
  next
    obtain g where "g \<in> totatives n" and "ord n g = Carmichael n"
      using Carmichael_root_exists[of n] \<open>n \<noteq> 0\<close> by auto
    thus "Carmichael n \<in> ord n ` totatives n" by force
  qed (use \<open>n \<noteq> 0\<close> in auto)
  thus ?thesis using False by simp
qed auto


subsection \<open>Existence of primitive roots for general moduli\<close>

text \<open>
  We now related Carmichael's function to the existence of primitive roots and, in the end,
  use this to show precisely which moduli have primitive roots and which do not.

  The first criterion for the existence of a primitive root is this: A primitive root modulo $n$
  exists iff $\lambda(n) = \varphi(n)$.
\<close>
lemma Carmichael_eq_totient_imp_primroot:
  assumes "n > 0" and "Carmichael n = totient n"
  shows   "\<exists>g. residue_primroot n g"
proof -
  from \<open>n > 0\<close> obtain g where "g \<in> totatives n" and "ord n g = Carmichael n"
    using Carmichael_root_exists[of n] by metis
  with assms show ?thesis by (auto simp: residue_primroot_def totatives_def coprime_commute)
qed

theorem residue_primroot_iff_Carmichael:
  "(\<exists>g. residue_primroot n g) \<longleftrightarrow> Carmichael n = totient n \<and> n > 0"
proof safe
  fix g assume g: "residue_primroot n g"
  thus "n > 0" by (auto simp: residue_primroot_def)
  have "coprime n g" by (rule ccontr) (use g in \<open>auto simp: residue_primroot_def\<close>)

  show "Carmichael n = totient n"
  proof (cases "n = 1")
    case False
    with \<open>n > 0\<close> have "n > 1" by auto
    with \<open>coprime n g\<close> have "ord n g dvd Carmichael n"
      by (intro ord_dvd_Carmichael) auto
    thus ?thesis using g by (intro dvd_antisym Carmichael_dvd_totient)
                            (auto simp: residue_primroot_def)
  qed auto
qed (use Carmichael_eq_totient_imp_primroot[of n] in auto)

text \<open>
  Any primitive root modulo $mn$ for coprime $m$, $n$ is also a primitive root modulo $m$ and $n$.
  The converse does not hold in general.
\<close>
lemma residue_primroot_modulus_mult_coprimeD:
  assumes "coprime m n" and "residue_primroot (m * n) g"
  shows   "residue_primroot m g" "residue_primroot n g"
proof -
  have *: "m > 0" "n > 0" "coprime m g" "coprime n g"
          "lcm (ord m g) (ord n g) = totient m * totient n"
    using assms
    by (auto simp: residue_primroot_def ord_modulus_mult_coprime totient_mult_coprime)

  define a b where "a = totient m div ord m g" and "b = totient n div ord n g"
  have ab: "totient m = ord m g * a" "totient n = ord n g * b"
    using * by (auto simp: a_def b_def order_divides_totient)

  have "a = 1" "b = 1" "coprime (ord m g) (ord n g)"
    unfolding coprime_iff_gcd_eq_1 using * by (auto simp: ab lcm_nat_def dvd_div_eq_mult ord_eq_0)
  with ab and * show "residue_primroot m g" "residue_primroot n g"
    by (auto simp: residue_primroot_def)
qed

text \<open>
  If a primitive root modulo $mn$ exists for coprime $m, n$, then $\lambda(m)$ and $\lambda(n)$
  must also be coprime. This is helpful in establishing that there are no primitive roots
  modulo $mn$ by showing e.\,g.\ that $\lambda(m)$ and $\lambda(n)$ are both even.
\<close>
lemma residue_primroot_modulus_mult_coprime_imp_Carmichael_coprime:
  assumes "coprime m n" and "residue_primroot (m * n) g"
  shows   "coprime (Carmichael m) (Carmichael n)"
proof -
  from residue_primroot_modulus_mult_coprimeD[OF assms]
    have *: "residue_primroot m g" "residue_primroot n g" by auto
  hence [simp]: "Carmichael m = totient m" "Carmichael n = totient n"
    by (simp_all add: residue_primroot_Carmichael)
  from * have mn: "m > 0" "n > 0" by (auto simp: residue_primroot_def)
  
  from assms have "Carmichael (m * n) = totient (m * n) \<and> n > 0"
    using residue_primroot_iff_Carmichael[of "m * n"] by auto
  with assms have "lcm (totient m) (totient n) = totient m * totient n"
    by (simp add: Carmichael_mult_coprime totient_mult_coprime)
  thus ?thesis unfolding coprime_iff_gcd_eq_1 using mn
    by (simp add: lcm_nat_def dvd_div_eq_mult)
qed
  
text \<open>
  The following moduli are precisely those that have primitive roots.
\<close>
definition cyclic_moduli :: "nat set" where
  "cyclic_moduli = {1, 2, 4} \<union> {p ^ k |p k. prime p \<and> odd p \<and> k > 0} \<union>
                     {2 * p ^ k |p k. prime p \<and> odd p \<and> k > 0}"

theorem residue_primroot_iff_in_cyclic_moduli:
  "(\<exists>g. residue_primroot m g) \<longleftrightarrow> m \<in> cyclic_moduli"
proof -
  have "(\<exists>g. residue_primroot m g)" if "m \<in> cyclic_moduli"
  using that unfolding cyclic_moduli_def
  by (intro Carmichael_eq_totient_imp_primroot)
     (auto dest: prime_gt_0_nat simp: Carmichael_prime_power totient_prime_power
                 Carmichael_mult_coprime totient_mult_coprime)

  moreover have "\<not>(\<exists>g. residue_primroot m g)" if "m \<notin> cyclic_moduli"
  proof (cases "m = 0")
    case False
    with that have [simp]: "m > 0" "m \<noteq> 1" by (auto simp: cyclic_moduli_def)
    show ?thesis
    proof (cases "\<exists>k. m = 2 ^ k")
      case True
      then obtain k where [simp]: "m = 2 ^ k" by auto
      with that have "k \<noteq> 0 \<and> k \<noteq> 1 \<and> k \<noteq> 2" by (auto simp: cyclic_moduli_def)
      hence "k \<ge> 3" by auto
      thus ?thesis by (subst residue_primroot_iff_Carmichael)
                      (auto simp: Carmichael_twopow totient_prime_power)
    next
      case False
      hence "\<exists>p\<in>prime_factors m. p \<noteq> 2"
        using Ex_other_prime_factor[of m 2] by auto
      from divide_out_primepow_ex[OF \<open>m \<noteq> 0\<close> this]
      obtain p k m' where p: "p \<noteq> 2" "prime p" "p dvd m" "\<not>p dvd m'" "0 < k" "m = p ^ k * m'"
        by metis
      have "odd p"
        using p primes_dvd_imp_eq[of 2 p] by auto
      from p have coprime: "coprime (p ^ k) m'"
        using p prime_imp_coprime by auto
      have "m \<in> cyclic_moduli" if "m' = 1"
        using that p \<open>odd p\<close> by (auto simp: cyclic_moduli_def)
      moreover have "m \<in> cyclic_moduli" if "m' = 2"
      proof -
        have "m = 2 * p ^ k" using p that by (simp add: mult.commute)
        thus "m \<in> cyclic_moduli" using p \<open>odd p\<close>
          unfolding cyclic_moduli_def by blast
      qed
      moreover have "m' \<noteq> 0" using p by (intro notI) auto
      ultimately have "m' \<noteq> 0 \<and>m' \<noteq> 1 \<and> m' \<noteq> 2" using that by auto
      hence "m' > 2" by linarith
  
      show ?thesis
      proof
        assume "\<exists>g. residue_primroot m g"
        with coprime p have coprime': "coprime (p - 1) (Carmichael m')"
          using residue_primroot_modulus_mult_coprime_imp_Carmichael_coprime[OF coprime]
          by (auto simp: Carmichael_prime_power)
        moreover have "even (p - 1)" "even (Carmichael m')"
          using \<open>m' > 2\<close> \<open>odd p\<close> by (auto intro!: even_Carmichael)
        ultimately show False by force
      qed
    qed
  qed auto

  ultimately show ?thesis by metis
qed

lemma residue_primroot_is_generator:
  assumes "m > 1" and "residue_primroot m g"
  shows   "bij_betw (\<lambda>i. g ^ i mod m) {..<totient m} (totatives m)"
  unfolding bij_betw_def
proof
  from assms have [simp]: "ord m g = totient m"
    by (simp add: residue_primroot_def)
  from assms have "coprime m g" by (simp add: residue_primroot_def)
  hence "inj_on (\<lambda>i. g ^ i mod m) {..<ord m g}"
    by (intro inj_power_mod)
  thus inj: "inj_on (\<lambda>i. g ^ i mod m) {..<totient m}"
    by simp

  show "(\<lambda>i. g ^ i mod m) ` {..<totient m} = totatives m"
  proof (rule card_subset_eq)
    show "card ((\<lambda>i. g ^ i mod m) ` {..<totient m}) = card (totatives m)"
      using inj by (subst card_image) (auto simp: totient_def)
    show "(\<lambda>i. g ^ i mod m) ` {..<totient m} \<subseteq> totatives m"
      using \<open>m > 1\<close> \<open>coprime m g\<close> power_in_totatives[of m g] by blast
  qed auto
qed

text \<open>
  Given one primitive root \<open>g\<close>, all the primitive roots are powers $g^i$ for
  $1\leq i \leq \varphi(n)$ with $\text{gcd}(i, \varphi(n)) = 1$.
\<close>
theorem residue_primroot_bij_betw_primroots:
  assumes "m > 1" and "residue_primroot m g"
  shows   "bij_betw (\<lambda>i. g ^ i mod m) (totatives (totient m))
                                      {g\<in>totatives m. residue_primroot m g}"
proof (cases "m = 2")
  case [simp]: True
  have [simp]: "totatives 2 = {1}"
    by (auto simp: totatives_def elim!: oddE)
  from assms have "odd g"
    by (auto simp: residue_primroot_def)
  hence pow_eq: "(\<lambda>i. g ^ i mod m) = (\<lambda>_. 1)"
    by (auto simp: fun_eq_iff mod_2_eq_odd)
  have "{g \<in> totatives m. residue_primroot m g} = {1}"
    by (auto simp: residue_primroot_def)
  thus ?thesis using pow_eq by (auto simp: bij_betw_def)
next
  case False
  thus ?thesis unfolding bij_betw_def
  proof safe
    from assms False have "m > 2" by auto
    from assms \<open>m > 2\<close> have "totient m > 1" by (intro totient_gt_1) auto
    from assms have [simp]: "ord m g = totient m"
      by (simp add: residue_primroot_def)
    from assms have "coprime m g" by (simp add: residue_primroot_def)
    hence "inj_on (\<lambda>i. g ^ i mod m) {..<ord m g}"
      by (intro inj_power_mod)
    thus "inj_on (\<lambda>i. g ^ i mod m) (totatives (totient m))"
      by (rule inj_on_subset)
         (use assms \<open>totient m > 1\<close> in \<open>auto simp: totatives_less residue_primroot_def\<close>)

    {
      fix i assume i: "i \<in> totatives (totient m)"
      from \<open>coprime m g\<close> and \<open>m > 2\<close> show "g ^ i mod m \<in> totatives m"
        by (intro power_in_totatives) auto
      show "residue_primroot m (g ^ i mod m)"
        using i \<open>m > 2\<close> \<open>coprime m g\<close>
        by (auto simp: residue_primroot_def coprime_commute ord_power totatives_def)
    }
    {
      fix x assume x: "x \<in> totatives m" "residue_primroot m x"
      then obtain i where i: "i < totient m" "x = (g ^ i mod m)"
        using assms residue_primroot_is_generator[of m g] by (auto simp: bij_betw_def)
      from i x \<open>m > 2\<close> have "i > 0" by (intro Nat.gr0I) (auto simp: residue_primroot_1_iff)
      have "totient m div gcd i (totient m) = totient m"
        using x i \<open>coprime m g\<close> by (auto simp add: residue_primroot_def ord_power)
      hence "coprime i (totient m)"
        unfolding coprime_iff_gcd_eq_1 using assms by (subst (asm) dvd_div_eq_mult) auto
      with i \<open>i > 0\<close> have "i \<in> totatives (totient m)" by (auto simp: totatives_def)
      thus "x \<in> (\<lambda>i. g ^ i mod m) ` totatives (totient m)" using i by auto
    }
  qed
qed

text \<open>
  It follows from the above statement that any residue ring modulo \<open>n\<close> that \<^emph>\<open>has\<close> primitive roots
  has exactly $\varphi(\varphi(n))$ of them.
\<close>
corollary card_residue_primroots:
  assumes "\<exists>g. residue_primroot m g"
  shows   "card {g\<in>totatives m. residue_primroot m g} = totient (totient m)"
proof (cases "m = 1")
  case [simp]: True
  have "{g \<in> totatives m. residue_primroot m g} = {1}"
    by (auto simp: residue_primroot_def)
  thus ?thesis by simp
next
  case False
  from assms obtain g where g: "residue_primroot m g" by auto
  hence "m \<noteq> 0" by (intro notI) auto
  with \<open>m \<noteq> 1\<close> have "m > 1" by linarith
  from this g have "bij_betw (\<lambda>i. g ^ i mod m) (totatives (totient m))
                      {g\<in>totatives m. residue_primroot m g}"
    by (rule residue_primroot_bij_betw_primroots)
  hence "card (totatives (totient m)) = card {g\<in>totatives m. residue_primroot m g}"
    by (rule bij_betw_same_card)
  thus ?thesis by (simp add: totient_def)
qed

corollary card_residue_primroots':
  "card {g\<in>totatives m. residue_primroot m g} =
     (if m \<in> cyclic_moduli then totient (totient m) else 0)"
  by (simp add: residue_primroot_iff_in_cyclic_moduli [symmetric] card_residue_primroots)

text \<open>
  As an example, we evaluate $\lambda(122200)$ using the prime factorisation.
\<close>
lemma "Carmichael 122200 = 1380"
proof -
  have "prime_factorization (2^3 * 5^2 * 13 * 47) = {#2, 2, 2, 5, 5, 13, 47::nat#}"
    by (intro prime_factorization_eqI) auto
  from eval_Carmichael[OF this] show "Carmichael 122200 = 1380"
    by (simp add: lcm_nat_def gcd_non_0_nat)
qed

(* TODO: definition of index ("discrete logarithm") *)

end