Quelle  Multiplicative_Group.thy

(*  Title:      HOL/Algebra/Multiplicative_Group.thy
  Author: Simon Wimmer
  Author: Lars Noschinski
*)

theory Multiplicative_Group
imports
  Complex_Main
  Group
  Coset
  UnivPoly
  Generated_Groups
  Elementary_Groups
begin

section ‹Simplification Rules for Polynomials›
text_raw ‹\label{sec:simp-rules}›

lemma (in ring_hom_cring) hom_sub[simp]:
  assumes "x ∈ carrier R" "y ∈ carrier R"
  shows "h (x ⊖ y) = h x ⊖🪙S🪙 h y"
  using assms by (simp add: R.minus_eq S.minus_eq)

context UP_ring begin

lemma deg_nzero_nzero:
  assumes deg_p_nzero: "deg R p ≠ 0"
  shows "p ≠ 0🪙P🪙"
  using deg_zero deg_p_nzero by auto

lemma deg_add_eq:
  assumes c: "p ∈ carrier P" "q ∈ carrier P"
  assumes "deg R q ≠ deg R p"
  shows "deg R (p ⊕🪙P🪙 q) = max (deg R p) (deg R q)"
proof -
  let ?m = "max (deg R p) (deg R q)"
  from assms have "coeff P p ?m = 0 ⟷ coeff P q ?m ≠ 0"
    by (metis deg_belowI lcoeff_nonzero[OF deg_nzero_nzero] linear max.absorb_iff2 max.absorb1)
  then have "coeff P (p ⊕🪙P🪙 q) ?m ≠ 0"
    using assms by auto
  then have "deg R (p ⊕🪙P🪙 q) ≥ ?m"
    using assms by (blast intro: deg_belowI)
  with deg_add[OF c] show ?thesis by arith
qed

lemma deg_minus_eq:
  assumes "p ∈ carrier P" "q ∈ carrier P" "deg R q ≠ deg R p"
  shows "deg R (p ⊖🪙P🪙 q) = max (deg R p) (deg R q)"
  using assms by (simp add: deg_add_eq a_minus_def)

end

context UP_cring begin

lemma evalRR_add:
  assumes "p ∈ carrier P" "q ∈ carrier P"
  assumes x: "x ∈ carrier R"
  shows "eval R R id x (p ⊕🪙P🪙 q) = eval R R id x p ⊕ eval R R id x q"
proof -
  interpret UP_pre_univ_prop R R id by unfold_locales simp
  interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
  show ?thesis using assms by simp
qed

lemma evalRR_sub:
  assumes "p ∈ carrier P" "q ∈ carrier P"
  assumes x: "x ∈ carrier R"
  shows "eval R R id x (p ⊖🪙P🪙 q) = eval R R id x p ⊖ eval R R id x q"
proof -
  interpret UP_pre_univ_prop R R id by unfold_locales simp
  interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
  show ?thesis using assms by simp
qed

lemma evalRR_mult:
  assumes "p ∈ carrier P" "q ∈ carrier P"
  assumes x: "x ∈ carrier R"
  shows "eval R R id x (p ⊗🪙P🪙 q) = eval R R id x p ⊗ eval R R id x q"
proof -
  interpret UP_pre_univ_prop R R id by unfold_locales simp
  interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
  show ?thesis using assms by simp
qed

lemma evalRR_monom:
  assumes a: "a ∈ carrier R" and x: "x ∈ carrier R"
  shows "eval R R id x (monom P a d) = a ⊗ x [^] d"
proof -
  interpret UP_pre_univ_prop R R id by unfold_locales simp
  show ?thesis using assms by (simp add: eval_monom)
qed

lemma evalRR_one:
  assumes x: "x ∈ carrier R"
  shows "eval R R id x 1🪙P🪙 = 1"
proof -
  interpret UP_pre_univ_prop R R id by unfold_locales simp
  interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
  show ?thesis using assms by simp
qed

lemma carrier_evalRR:
  assumes x: "x ∈ carrier R" and "p ∈ carrier P"
  shows "eval R R id x p ∈ carrier R"
proof -
  interpret UP_pre_univ_prop R R id by unfold_locales simp
  interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
  show ?thesis using assms by simp
qed

lemmas evalRR_simps = evalRR_add evalRR_sub evalRR_mult evalRR_monom evalRR_one carrier_evalRR

end



section ‹Properties of the Euler ‹φ›-function›
text_raw ‹\label{sec:euler-phi}›

text‹
  In this section we prove that for every positive natural number the equation
  $\sum_{d | n}^n \varphi(d) = n$ holds.
 ›

lemma dvd_div_ge_1:
  fixes a b :: nat
  assumes "a ≥ 1" "b dvd a"
  shows "a div b ≥ 1"
proof -
  from ‹b dvd a› obtain c where "a = b * c" ..
  with ‹a ≥ 1› show ?thesis by simp
qed

lemma dvd_nat_bounds:
 fixes n p :: nat
 assumes "p > 0" "n dvd p"
 shows "n > 0 ∧ n ≤ p"
 using assms by (simp add: dvd_pos_nat dvd_imp_le)

(* TODO FIXME: This is the "totient" function from HOL-Number_Theory, but since part of
  HOL-Number_Theory depends on HOL-Algebra.Multiplicative_Group, there would be a cyclic
   dependency. *)
definition phi' :: "nat => nat"
  where "phi' m = card {x. 1 ≤ x ∧ x ≤ m ∧ coprime x m}"

notation (latex output)
  phi' (‹φ _›)

lemma phi'_nonzero:
  assumes "m > 0"
  shows "phi' m > 0"
proof -
  have "1 ∈ {x. 1 ≤ x ∧ x ≤ m ∧ coprime x m}" using assms by simp
  hence "card {x. 1 ≤ x ∧ x ≤ m ∧ coprime x m} > 0" by (auto simp: card_gt_0_iff)
  thus ?thesis unfolding phi'_def by simp
qed

lemma dvd_div_eq_1:
  fixes a b c :: nat
  assumes "c dvd a" "c dvd b" "a div c = b div c"
  shows "a = b" using assms dvd_mult_div_cancel[OF ‹c dvd a›] dvd_mult_div_cancel[OF ‹c dvd b›]
                by presburger

lemma dvd_div_eq_2:
  fixes a b c :: nat
  assumes "c>0" "a dvd c" "b dvd c" "c div a = c div b"
  shows "a = b"
  proof -
  have "a > 0" "a ≤ c" using dvd_nat_bounds[OF assms(1-2)] by auto
  have "a*(c div a) = c" using assms dvd_mult_div_cancel by fastforce
  also have "… = b*(c div a)" using assms dvd_mult_div_cancel by fastforce
  finally show "a = b" using ‹c>0› dvd_div_ge_1[OF _ ‹a dvd c›] by fastforce
qed

lemma div_mult_mono:
  fixes a b c :: nat
  assumes "a > 0" "a≤d"
  shows "a * b div d ≤ b"
proof -
  have "a*b div d ≤ b*a div a" using assms div_le_mono2 mult.commute[of a b] by presburger
  thus ?thesis using assms by force
qed

text‹
  We arrive at the main result of this section:
  For every positive natural number the equation $\sum_{d | n}^n \varphi(d) = n$ holds.
 
  The outline of the proof for this lemma is as follows:
  We count the $n$ fractions $1/n$, $\ldots$, $(n-1)/n$, $n/n$.
  We analyze the reduced form $a/d = m/n$ for any of those fractions.
  We want to know how many fractions $m/n$ have the reduced form denominator $d$.
  The condition $1 \leq m \leq n$ is equivalent to the condition $1 \leq a \leq d$.
  Therefore we want to know how many $a$ with $1 \leq a \leq d$ exist, s.t. 🍋‹gcd a d = 1›.
  This number is exactly 🍋‹phi' d›.
 
  Finally, by counting the fractions $m/n$ according to their reduced form denominator,
  we get: @{term [display] "(∑d | d dvd n . phi' d) = n"}.
  To formalize this proof in Isabelle, we analyze for an arbitrary divisor $d$ of $n$
  \begin{itemize}
  \item the set of reduced form numerators 🍋‹{a. (1::nat) ≤ a ∧ a ≤ d ∧ coprime a d}›
  \item the set of numerators $m$, for which $m/n$ has the reduced form denominator $d$,
  i.e. the set 🍋‹{m ∈ {1::nat .. n}. n div gcd m n = d}›
  \end{itemize}
  We show that 🍋‹λa. a*n div d› with the inverse 🍋‹λa. a div gcd a n› is
  a bijection between theses sets, thus yielding the equality
  @{term [display] "phi' d = card {m ∈ {1 .. n}. n div gcd m n = d}"}
  This gives us
  @{term [display] "(∑d | d dvd n . phi' d)
  = card (∪d ∈ {d. d dvd n}. {m ∈ {1 .. n}. n div gcd m n = d})"}
  and by showing
  🍋‹(∪d ∈ {d. d dvd n}. {m ∈ {1::nat .. n}. n div gcd m n = d}) 🪙 {1 .. n}›
  (this is our counting argument) the thesis follows.
 ›
lemma sum_phi'_factors:
 fixes n :: nat
 assumes "n > 0"
 shows "(∑d | d dvd n. phi' d) = n"
proof -
  have "card {a. 1 ≤ a ∧ a ≤ d ∧ coprime a d} = card {m ∈ {1 .. n}. n div gcd m n = d}"
    (is "card ?RF = card ?F")
    if "d dvd n" for d
  proof (rule card_bij_eq)
    from that obtain q where q: "n = d * q" ..
    have "a = b" if "a * n div d = b * n div d" for a b
    proof -
      from that have "a * (n div d) = b * (n div d)"
        using dvd_div_mult[OF ‹d dvd n›] by (fastforce simp add: mult.commute)
      then show ?thesis using dvd_div_ge_1[OF _ ‹d dvd n›] ‹n>0›
        by (simp add: mult.commute nat_mult_eq_cancel1)
    qed
    thus "inj_on (λa. a*n div d) ?RF" unfolding inj_on_def by blast
    have "a * n div d ∈ ?F" if a: "a∈?RF" for a
    proof -
      from that have "a * (n div d) ≥ 1" using ‹n>0› dvd_div_ge_1[OF _ ‹d dvd n›] by simp
      hence ge_1: "a * n div d ≥ 1" by (simp add: ‹d dvd n› div_mult_swap)
      have le_n: "a * n div d ≤ n" using div_mult_mono a by simp
      have "gcd (a * n div d) n = n div d * gcd a d"
        by (simp add: gcd_mult_distrib_nat q ac_simps)
      hence "n div gcd (a * n div d) n = d*n div (d*(n div d))" using a by simp
      then show ?thesis
        using ge_1 le_n by (fastforce simp add: ‹d dvd n›)
    qed
    thus "(λa. a*n div d) ` ?RF ⊆ ?F" by blast
    have "m = l" if A: "m ∈ ?F" "l ∈ ?F" "m div gcd m n = l div gcd l n" for m l
    proof -
      from that have "gcd m n = gcd l n" using dvd_div_eq_2[OF assms] by fastforce
      then show ?thesis using dvd_div_eq_1[of "gcd m n" m l] A(3) by fastforce
    qed
    thus "inj_on (λa. a div gcd a n) ?F" unfolding inj_on_def by blast
    have "m div gcd m n ∈ ?RF" if "m ∈ ?F" for m
      using that dvd_div_ge_1  by (fastforce simp add: div_le_mono div_gcd_coprime)
    thus "(λa. a div gcd a n) ` ?F ⊆ ?RF" by blast
  qed force+
  hence phi'_eq: "∧d. d dvd n ==> phi' d = card {m ∈ {1 .. n}. n div gcd m n = d}"
    unfolding phi'_def by presburger
  have fin: "finite {d. d dvd n}" using dvd_nat_bounds[OF ‹n>0›] by force
  have "(∑d | d dvd n. phi' d)
                 = card (∪d ∈ {d. d dvd n}. {m ∈ {1 .. n}. n div gcd m n = d})"
    using card_UN_disjoint[OF fin, of "(λd. {m ∈ {1 .. n}. n div gcd m n = d})"] phi'_eq
    by fastforce
  also have "(∪d ∈ {d. d dvd n}. {m ∈ {1 .. n}. n div gcd m n = d}) = {1 .. n}" (is "?L = ?R")
  proof
    show "?L 🪙 ?R"
    proof
      fix m assume m: "m ∈ ?R"
      thus "m ∈ ?L" using dvd_triv_right[of "n div gcd m n" "gcd m n"]
        by simp
    qed
  qed fastforce
  finally show ?thesis by force
qed



section ‹Order of an Element of a Group›
text_raw ‹\label{sec:order-elem}›


context group begin

definition (in group) ord :: "'a ==> nat" where
  "ord x ≡ (@d. ∀n::nat. x [^] n = 1 ⟷ d dvd n)"

lemma (in group) pow_eq_id:
  assumes "x ∈ carrier G"
  shows "x [^] n = 1 ⟷ (ord x) dvd n"
proof (cases "∀n::nat. pow G x n = one G ⟶ n = 0")
  case True
  show ?thesis
    unfolding ord_def
    by (rule someI2 [where a=0]) (auto simp: True)
next
  case False
  define N where "N ≡ LEAST n::nat. x [^] n = 1 ∧ n > 0"
  have N: "x [^] N = 1 ∧ N > 0"
    using False
    apply (simp add: N_def)
    by (metis (mono_tags, lifting) LeastI)
  have eq0: "n = 0" if "x [^] n = 1" "n < N" for n
    using N_def not_less_Least that by fastforce
  show ?thesis
    unfolding ord_def
  proof (rule someI2 [where a = N], rule allI)
    fix n :: "nat"
    show "(x [^] n = 1) ⟷ (N dvd n)"
    proof (cases "n = 0")
      case False
      show ?thesis
        unfolding dvd_def
      proof safe
        assume 1: "x [^] n = 1"
        have "x [^] n = x [^] (n mod N + N * (n div N))"
          by simp
        also have "… = x [^] (n mod N) ⊗ x [^] (N * (n div N))"
          by (simp add: assms nat_pow_mult)
        also have "… = x [^] (n mod N)"
          by (metis N assms l_cancel_one nat_pow_closed nat_pow_one nat_pow_pow)
        finally have "x [^] (n mod N) = 1"
          by (simp add: "1")
        then have "n mod N = 0"
          using N eq0 mod_less_divisor by blast
        then show "∃k. n = N * k"
          by blast
      next
        fix k :: "nat"
        assume "n = N * k"
        with N show "x [^] (N * k) = 1"
          by (metis assms nat_pow_one nat_pow_pow)
      qed
    qed simp
  qed blast
qed

lemma (in group) pow_ord_eq_1 [simp]:
   "x ∈ carrier G ==> x [^] ord x = 1"
  by (simp add: pow_eq_id)

lemma (in group) int_pow_eq_id:
  assumes "x ∈ carrier G"
  shows "(pow G x i = one G ⟷ int (ord x) dvd i)"
proof (cases i rule: int_cases2)
  case (nonneg n)
  then show ?thesis
    by (simp add: int_pow_int pow_eq_id assms)
next
  case (nonpos n)
  then have "x [^] i = inv (x [^] n)"
    by (simp add: assms int_pow_int int_pow_neg)
  then show ?thesis
    by (simp add: assms pow_eq_id nonpos)
qed

lemma (in group) int_pow_eq:
   "x ∈ carrier G ==> (x [^] m = x [^] n) ⟷ int (ord x) dvd (n - m)"
  apply (simp flip: int_pow_eq_id)
  by (metis int_pow_closed int_pow_diff inv_closed r_inv right_cancel)

lemma (in group) ord_eq_0:
   "x ∈ carrier G ==> (ord x = 0 ⟷ (∀n::nat. n ≠ 0 ⟶ x [^] n ≠ 1))"
  by (auto simp: pow_eq_id)

lemma (in group) ord_unique:
   "x ∈ carrier G ==> ord x = d ⟷ (∀n. pow G x n = one G ⟷ d dvd n)"
  by (meson dvd_antisym dvd_refl pow_eq_id)

lemma (in group) ord_eq_1:
   "x ∈ carrier G ==> (ord x = 1 ⟷ x = 1)"
  by (metis pow_eq_id nat_dvd_1_iff_1 nat_pow_eone)

lemma (in group) ord_id [simp]:
   "ord (one G) = 1"
  using ord_eq_1 by blast

lemma (in group) ord_inv [simp]:
   "x ∈ carrier G
        ==> ord (m_inv G x) = ord x"
  by (simp add: ord_unique pow_eq_id nat_pow_inv)

lemma (in group) ord_pow:
  assumes "x ∈ carrier G" "k dvd ord x" "k ≠ 0"
  shows "ord (pow G x k) = ord x div k"
proof -
  have "(x [^] k) [^] (ord x div k) = 1"
    using assms by (simp add: nat_pow_pow)
  moreover have "ord x dvd k * ord (x [^] k)"
    by (metis assms(1) pow_ord_eq_1 pow_eq_id nat_pow_closed nat_pow_pow)
  ultimately show ?thesis
    by (metis assms div_dvd_div dvd_antisym dvd_triv_left pow_eq_id nat_pow_closed nonzero_mult_div_cancel_left)
qed

lemma (in group) ord_mul_divides:
  assumes eq: "x ⊗ y = y ⊗ x" and xy: "x ∈ carrier G" "y ∈ carrier G"
  shows "ord (x ⊗ y) dvd (ord x * ord y)"
apply (simp add: xy flip: pow_eq_id eq)
  by (metis dvd_triv_left dvd_triv_right eq pow_eq_id one_closed pow_mult_distrib r_one xy)

lemma (in comm_group) abelian_ord_mul_divides:
   "[x ∈ carrier G; y ∈ carrier G]
        ==> ord (x ⊗ y) dvd (ord x * ord y)"
  by (simp add: ord_mul_divides m_comm)

lemma ord_inj:
  assumes a: "a ∈ carrier G"
  shows "inj_on (λ x . a [^] x) {0 .. ord a - 1}"
proof -
  let ?M = "Max (ord ` carrier G)"
  have "finite {d ∈ {..?M}. a [^] d = 1}" by auto

  have *: False if A: "x < y" "x ∈ {0 .. ord a - 1}" "y ∈ {0 .. ord a - 1}"
        "a [^] x = a [^] y" for x y
  proof -
    have "y - x < ord a" using that by auto
    moreover have "a [^] (y-x) = 1" using a A by (simp add: pow_eq_div2)
    ultimately have "min (y - x) (ord a) = ord a"
      using A(1) a pow_eq_id by auto
    with ‹y - x 🚫 a› show False by linarith
  qed
  show ?thesis
    unfolding inj_on_def by (metis nat_neq_iff *)
qed

lemma ord_inj':
  assumes a: "a ∈ carrier G"
  shows "inj_on (λ x . a [^] x) {1 .. ord a}"
proof (rule inj_onI, rule ccontr)
  fix x y :: nat
  assume A: "x ∈ {1 .. ord a}" "y ∈ {1 .. ord a}" "a [^] x = a [^] y" "x≠y"
  then consider "x < ord a" "y < ord a" | "x = ord a" "y < ord a" | "y = ord a" "x < ord a"
    by force
  then show False
  proof cases
    case 1
    then show ?thesis using ord_inj[OF assms] A unfolding inj_on_def by fastforce
  next
    case 2
    hence "a [^] y = a [^] (0::nat)" using pow_ord_eq_1 A by (simp add: a)
    hence "y=0" using ord_inj[OF assms] ‹y 🚫 a› unfolding inj_on_def by force
    with A show ?thesis by fastforce
  next
    case 3
    hence "a [^] x = a [^] (0::nat)" using pow_ord_eq_1 A by (simp add: a)
    hence "x=0" using ord_inj[OF assms] ‹x 🚫 a› unfolding inj_on_def by force
    with A show ?thesis by fastforce
  qed
qed

lemma (in group) ord_ge_1: 
  assumes finite: "finite (carrier G)" and a: "a ∈ carrier G"
  shows "ord a ≥ 1" 
proof -
  have "((λn::nat. a [^] n) ` {0<..}) ⊆ carrier G"
    using a by blast
  then have "finite ((λn::nat. a [^] n) ` {0<..})"
    using finite_subset finite by auto
  then have "¬ inj_on (λn::nat. a [^] n) {0<..}"
    using finite_imageD infinite_Ioi by blast
  then obtain i j::nat where "i ≠ j" "a [^] i = a [^] j"
    by (auto simp: inj_on_def)
  then have "∃n::nat. n>0 ∧ a [^] n = 1"
    by (metis a diffs0_imp_equal pow_eq_div2 neq0_conv)
  then have "ord a ≠ 0"
    by (simp add: ord_eq_0 [OF a])
  then show ?thesis
    by simp
qed

lemma ord_elems:
  assumes "finite (carrier G)" "a ∈ carrier G"
  shows "{a[^]x | x. x ∈ (UNIV :: nat set)} = {a[^]x | x. x ∈ {0 .. ord a - 1}}" (is "?L = ?R")
proof
  show "?R ⊆ ?L" by blast
  have "y ∈ {a[^]x | x. x ∈ {0 .. ord a - 1}}" if "y ∈ ?L" for y
  proof -
    from that obtain x::nat where x: "y = a[^]x" by auto
    define r q where "r = x mod ord a" and "q = x div ord a"
    then have "x = q * ord a + r"
      by (simp add: div_mult_mod_eq)
    hence "y = (a[^]ord a)[^]q ⊗ a[^]r"
      using x assms by (metis mult.commute nat_pow_mult nat_pow_pow)
    hence "y = a[^]r" using assms by (simp add: pow_ord_eq_1)
    have "r < ord a" using ord_ge_1[OF assms] by (simp add: r_def)
    hence "r ∈ {0 .. ord a - 1}" by (force simp: r_def)
    thus ?thesis using ‹y=a[^]r› by blast
  qed
  thus "?L ⊆ ?R" by auto
qed

lemma (in group)
  assumes "x ∈ carrier G"
  shows finite_cyclic_subgroup:
        "finite(carrier(subgroup_generated G {x})) ⟷ (∃n::nat. n ≠ 0 ∧ x [^] n = 1)" (is "?fin ⟷ ?nat1")
    and infinite_cyclic_subgroup:
        "infinite(carrier(subgroup_generated G {x})) ⟷ (∀m n::nat. x [^] m = x [^] n ⟶ m = n)" (is "¬ ?fin ⟷ ?nateq")
    and finite_cyclic_subgroup_int:
        "finite(carrier(subgroup_generated G {x})) ⟷ (∃i::int. i ≠ 0 ∧ x [^] i = 1)" (is "?fin ⟷ ?int1")
    and infinite_cyclic_subgroup_int:
        "infinite(carrier(subgroup_generated G {x})) ⟷ (∀i j::int. x [^] i = x [^] j ⟶ i = j)" (is "¬ ?fin ⟷ ?inteq")
proof -
  have 1: "¬ ?fin" if ?nateq
  proof -
    have "infinite (range (λn::nat. x [^] n))"
      using that range_inj_infinite [of "(λn::nat. x [^] n)"] by (auto simp: inj_on_def)
    moreover have "range (λn::nat. x [^] n) ⊆ range (λi::int. x [^] i)"
      apply clarify
      by (metis assms group.int_pow_neg int_pow_closed int_pow_neg_int is_group local.inv_equality nat_pow_closed r_inv rangeI)
    ultimately show ?thesis
      using carrier_subgroup_generated_by_singleton [OF assms] finite_subset by auto
  qed
  have 2: "m = n" if mn: "x [^] m = x [^] n" and eq [rule_format]: "?inteq" for m n::nat
    using eq [of "int m" "int n"]
    by (simp add: int_pow_int mn)
  have 3: ?nat1 if non: "¬ ?inteq"
  proof -
    obtain i j::int where eq: "x [^] i = x [^] j" and "i ≠ j"
      using non by auto
    show ?thesis
    proof (cases i j rule: linorder_cases)
      case less
      then have [simp]: "x [^] (j - i) = 1"
        by (simp add: eq assms int_pow_diff)
      show ?thesis
        using less by (rule_tac x="nat (j-i)" in exI) auto
    next
      case greater
      then have [simp]: "x [^] (i - j) = 1"
        by (simp add: eq assms int_pow_diff)
      then show ?thesis
        using greater by (rule_tac x="nat (i-j)" in exI) auto
    qed (use ‹i ≠ j› in auto)
  qed
  have 4: "∃i::int. (i ≠ 0) ∧ x [^] i = 1" if "n ≠ 0" "x [^] n = 1" for n::nat
    apply (rule_tac x="int n" in exI)
    by (simp add: int_pow_int that)
  have 5: "finite (carrier (subgroup_generated G {x}))" if "i ≠ 0" and 1: "x [^] i = 1" for i::int
  proof -
    obtain n::nat where n: "n > 0" "x [^] n = 1"
      using "1" "3" ‹i ≠ 0› by fastforce
    have "x [^] a ∈ ([^]) x ` {0.. for a::int
    proof
      show "x [^] a = x [^] nat (a mod int n)"
        using n
        by simp (metis (no_types, lifting) assms dvd_minus_mod dvd_trans int_pow_eq int_pow_eq_id int_pow_int)
      show "nat (a mod int n) ∈ {0..
        using n by (simp add: nat_less_iff)
    qed
    then have "carrier (subgroup_generated G {x}) ⊆ ([^]) x ` {0..
      using carrier_subgroup_generated_by_singleton [OF assms] by auto
    then show ?thesis
      using finite_surj by blast
  qed
  show "?fin ⟷ ?nat1" "¬ ?fin ⟷ ?nateq" "?fin ⟷ ?int1" "¬ ?fin ⟷ ?inteq"
    using 1 2 3 4 5 by meson+
qed

lemma (in group) finite_cyclic_subgroup_order:
   "x ∈ carrier G ==> finite(carrier(subgroup_generated G {x})) ⟷ ord x ≠ 0"
  by (simp add: finite_cyclic_subgroup ord_eq_0)

lemma (in group) infinite_cyclic_subgroup_order:
   "x ∈ carrier G ==> infinite (carrier(subgroup_generated G {x})) ⟷ ord x = 0"
  by (simp add: finite_cyclic_subgroup_order)

lemma generate_pow_on_finite_carrier: 🍋‹contributor ‹Paulo Emílio de Vilhena›\›
  assumes "finite (carrier G)" and a: "a ∈ carrier G"
  shows "generate G { a } = { a [^] k | k. k ∈ (UNIV :: nat set) }"
proof
  show "{ a [^] k | k. k ∈ (UNIV :: nat set) } ⊆ generate G { a }"
  proof
    fix b assume "b ∈ { a [^] k | k. k ∈ (UNIV :: nat set) }"
    then obtain k :: nat where "b = a [^] k" by blast
    hence "b = a [^] (int k)"
      by (simp add: int_pow_int)
    thus "b ∈ generate G { a }"
      unfolding generate_pow[OF a] by blast
  qed
next
  show "generate G { a } ⊆ { a [^] k | k. k ∈ (UNIV :: nat set) }"
  proof
    fix b assume "b ∈ generate G { a }"
    then obtain k :: int where k: "b = a [^] k"
      unfolding generate_pow[OF a] by blast
    show "b ∈ { a [^] k | k. k ∈ (UNIV :: nat set) }"
    proof (cases "k < 0")
      assume "¬ k < 0"
      hence "b = a [^] (nat k)"
        by (simp add: k)
      thus ?thesis by blast
    next
      assume "k < 0"
      hence b: "b = inv (a [^] (nat (- k)))"
        using k a by (auto simp: int_pow_neg)
      obtain m where m: "ord a * m ≥ nat (- k)"
        by (metis assms mult.left_neutral mult_le_mono1 ord_ge_1)
      hence "a [^] (ord a * m) = 1"
        by (metis a nat_pow_one nat_pow_pow pow_ord_eq_1)
      then obtain k' :: nat where "(a [^] (nat (- k))) ⊗ (a [^] k') = 1"
        using m a nat_le_iff_add nat_pow_mult by auto
      hence "b = a [^] k'"
        using b a by (metis inv_unique' nat_pow_closed nat_pow_comm)
      thus "b ∈ { a [^] k | k. k ∈ (UNIV :: nat set) }" by blast
    qed
  qed
qed

lemma ord_elems_inf_carrier:
 assumes "a ∈ carrier G" "ord a ≠ 0"
 shows "{a[^]x | x. x ∈ (UNIV :: nat set)} = {a[^]x | x. x ∈ {0 .. ord a - 1}}" (is "?L = ?R")
proof
  show "?R ⊆ ?L" by blast
  have "y ∈ {a[^]x | x. x ∈ {0 .. ord a - 1}}" if "y ∈ ?L" for y
  proof -
    from that obtain x::nat where x: "y = a[^]x" by auto
    define r q where "r = x mod ord a" and "q = x div ord a"
    then have "x = q * ord a + r"
      by (simp add: div_mult_mod_eq)
    hence "y = (a[^]ord a)[^]q ⊗ a[^]r"
      using x assms by (metis mult.commute nat_pow_mult nat_pow_pow)
    hence "y = a[^]r" using assms by simp
    have "r < ord a" using assms by (simp add: r_def)
    hence "r ∈ {0 .. ord a - 1}" by (force simp: r_def)
    then show ?thesis using ‹y=a[^]r› by blast
  qed
  thus "?L ⊆ ?R" by auto
qed

lemma generate_pow_nat:
 assumes a: "a ∈ carrier G" and "ord a ≠ 0"
 shows "generate G { a } = { a [^] k | k. k ∈ (UNIV :: nat set) }"
proof
 show "{ a [^] k | k. k ∈ (UNIV :: nat set) } ⊆ generate G { a }"
 proof
   fix b assume "b ∈ { a [^] k | k. k ∈ (UNIV :: nat set) }"
   then obtain k :: nat where "b = a [^] k" by blast
   hence "b = a [^] (int k)"
     by (simp add: int_pow_int)
   thus "b ∈ generate G { a }"
     unfolding generate_pow[OF a] by blast
 qed
next
 show "generate G { a } ⊆ { a [^] k | k. k ∈ (UNIV :: nat set) }"
 proof
   fix b assume "b ∈ generate G { a }"
   then obtain k :: int where k: "b = a [^] k"
     unfolding generate_pow[OF a] by blast
   show "b ∈ { a [^] k | k. k ∈ (UNIV :: nat set) }"
   proof (cases "k < 0")
     assume "¬ k < 0"
     hence "b = a [^] (nat k)"
       by (simp add: k)
     thus ?thesis by blast
   next
     assume "k < 0"
     hence b: "b = inv (a [^] (nat (- k)))"
       using k a by (auto simp: int_pow_neg)
     obtain m where m: "ord a * m ≥ nat (- k)"
       by (metis assms(2) dvd_imp_le dvd_triv_right le_zero_eq mult_eq_0_iff not_gr_zero)
     hence "a [^] (ord a * m) = 1"
       by (metis a nat_pow_one nat_pow_pow pow_ord_eq_1)
     then obtain k' :: nat where "(a [^] (nat (- k))) ⊗ (a [^] k') = 1"
       using m a nat_le_iff_add nat_pow_mult by auto
     hence "b = a [^] k'"
       using b a by (metis inv_unique' nat_pow_closed nat_pow_comm)
     thus "b ∈ { a [^] k | k. k ∈ (UNIV :: nat set) }" by blast
   qed
 qed
qed

lemma generate_pow_card:
  assumes a: "a ∈ carrier G"
  shows "ord a = card (generate G { a })"
proof (cases "ord a = 0")
  case True
  then have "infinite (carrier (subgroup_generated G {a}))"
    using infinite_cyclic_subgroup_order[OF a] by auto
  then have "infinite (generate G {a})"
    unfolding subgroup_generated_def
    using a by simp
  then show ?thesis
    using ‹ord a = 0› by auto
next
  case finite_subgroup: False
  then have "generate G { a } = (([^]) a) ` {0..ord a - 1}"
    using generate_pow_nat ord_elems_inf_carrier a by auto
  hence "card (generate G {a}) = card {0..ord a - 1}"
    using ord_inj[OF a] card_image by metis
  also have "... = ord a" using finite_subgroup by auto
  finally show ?thesis.. 
qed

lemma (in group) cyclic_order_is_ord:
 assumes "g ∈ carrier G"
 shows "ord g = order (subgroup_generated G {g})"
 unfolding order_def subgroup_generated_def
 using assms generate_pow_card by simp

lemma ord_dvd_group_order:
  assumes "a ∈ carrier G" shows "(ord a) dvd (order G)"
  using lagrange[OF generate_is_subgroup[of "{a}"]] assms
  unfolding generate_pow_card[OF assms]
  by (metis dvd_triv_right empty_subsetI insert_subset)

lemma (in group) pow_order_eq_1:
  assumes "a ∈ carrier G" shows "a [^] order G = 1"
  using assms by (metis nat_pow_pow ord_dvd_group_order pow_ord_eq_1 dvdE nat_pow_one)

lemma dvd_gcd:
  fixes a b :: nat
  obtains q where "a * (b div gcd a b) = b*q"
proof
  have "a * (b div gcd a b) = (a div gcd a b) * b" by (simp add:  div_mult_swap dvd_div_mult)
  also have "… = b * (a div gcd a b)" by simp
  finally show "a * (b div gcd a b) = b * (a div gcd a b) " .
qed

lemma (in group) ord_le_group_order:
  assumes finite: "finite (carrier G)" and a: "a ∈ carrier G"
  shows "ord a ≤ order G"
  by (simp add: a dvd_imp_le local.finite ord_dvd_group_order order_gt_0_iff_finite)

lemma (in group) ord_pow_gen:
  assumes "x ∈ carrier G"
  shows "ord (pow G x k) = (if k = 0 then 1 else ord x div gcd (ord x) k)"
proof -
  have "ord (x [^] k) = ord x div gcd (ord x) k"
    if "0 < k"
  proof -
    have "(d dvd k * n) = (d div gcd (d) k dvd n)" for d n
      using that by (simp add: div_dvd_iff_mult gcd_mult_distrib_nat mult.commute)
    then show ?thesis
      using that by (auto simp add: assms ord_unique nat_pow_pow pow_eq_id)
  qed
  then show ?thesis by auto
qed

lemma (in group)
  assumes finite': "finite (carrier G)" "a ∈ carrier G"
  shows pow_ord_eq_ord_iff: "group.ord G (a [^] k) = ord a ⟷ coprime k (ord a)" (is "?L ⟷ ?R")
    using assms ord_ge_1 [OF assms]
    by (auto simp: div_eq_dividend_iff ord_pow_gen coprime_iff_gcd_eq_1 gcd.commute split: if_split_asm)

lemma element_generates_subgroup:
  assumes finite[simp]: "finite (carrier G)"
  assumes a[simp]: "a ∈ carrier G"
  shows "subgroup {a [^] i | i. i ∈ {0 .. ord a - 1}} G"
  using generate_is_subgroup[of "{ a }"] assms(2)
        generate_pow_on_finite_carrier[OF assms]
  unfolding ord_elems[OF assms] by auto

end


section ‹Number of Roots of a Polynomial›
text_raw ‹\label{sec:number-roots}›


definition mult_of :: "('a, 'b) ring_scheme ==> 'a monoid" where
  "mult_of R ≡ ( carrier = carrier R - {0🪙R🪙}, mult = mult R, one = 1🪙R🪙)"

lemma carrier_mult_of [simp]: "carrier (mult_of R) = carrier R - {0🪙R🪙}"
  by (simp add: mult_of_def)

lemma mult_mult_of [simp]: "mult (mult_of R) = mult R"
 by (simp add: mult_of_def)

lemma nat_pow_mult_of: "([^]🪙mult_of R🪙) = (([^]🪙R🪙) :: _ ==> nat ==> _)"
  by (simp add: mult_of_def fun_eq_iff nat_pow_def)

lemma one_mult_of [simp]: "1🪙mult_of R🪙 = 1🪙R🪙"
  by (simp add: mult_of_def)

lemmas mult_of_simps = carrier_mult_of mult_mult_of nat_pow_mult_of one_mult_of

context field
begin

lemma mult_of_is_Units: "mult_of R = units_of R"
  unfolding mult_of_def units_of_def using field_Units by auto

lemma m_inv_mult_of:
"∧x. x ∈ carrier (mult_of R) ==> m_inv (mult_of R) x = m_inv R x"
  using mult_of_is_Units units_of_inv unfolding units_of_def
  by simp

lemma (in field) field_mult_group: "group (mult_of R)"
  proof (rule groupI)
  show "∃y∈carrier (mult_of R). y ⊗🪙mult_of R🪙 x = 1🪙mult_of R🪙"
    if "x ∈ carrier (mult_of R)" for x
    using group.l_inv_ex mult_of_is_Units that units_group by fastforce
qed (auto simp: m_assoc dest: integral)

lemma finite_mult_of: "finite (carrier R) ==> finite (carrier (mult_of R))"
  by simp

lemma order_mult_of: "finite (carrier R) ==> order (mult_of R) = order R - 1"
  unfolding order_def carrier_mult_of by (simp add: card.remove)

end



lemma (in monoid) Units_pow_closed :
  fixes d :: nat
  assumes "x ∈ Units G"
  shows "x [^] d ∈ Units G"
    by (metis assms group.is_monoid monoid.nat_pow_closed units_group units_of_carrier units_of_pow)

lemma (in ring) r_right_minus_eq[simp]:
  assumes "a ∈ carrier R" "b ∈ carrier R"
  shows "a ⊖ b = 0 ⟷ a = b"
  using assms by (metis a_minus_def add.inv_closed minus_equality r_neg)

context UP_cring begin

lemma is_UP_cring: "UP_cring R" by (unfold_locales)
lemma is_UP_ring:
  shows "UP_ring R" by (unfold_locales)

end

context UP_domain begin


lemma roots_bound:
  assumes f [simp]: "f ∈ carrier P"
  assumes f_not_zero: "f ≠ 0🪙P🪙"
  assumes finite: "finite (carrier R)"
  shows "finite {a ∈ carrier R . eval R R id a f = 0} ∧
         card {a ∈ carrier R . eval R R id a f = 0} ≤ deg R f" using f f_not_zero
proof (induction "deg R f" arbitrary: f)
  case 0
  have "∧x. eval R R id x f ≠ 0"
  proof -
    fix x
    have "(⨁i∈{..deg R f}. id (coeff P f i) ⊗ x [^] i) ≠ 0"
      using 0 lcoeff_nonzero_nonzero[where p = f] by simp
    thus "eval R R id x f ≠ 0" using 0 unfolding eval_def P_def by simp
  qed
  then have *: "{a ∈ carrier R. eval R R (λa. a) a f = 0} = {}"
    by (auto simp: id_def)
  show ?case by (simp add: *)
next
  case (Suc x)
  show ?case
  proof (cases "∃ a ∈ carrier R . eval R R id a f = 0")
    case True
    then obtain a where a_carrier[simp]: "a ∈ carrier R" and a_root: "eval R R id a f = 0" by blast
    have R_not_triv: "carrier R ≠ {0}"
      by (metis R.one_zeroI R.zero_not_one)
    obtain q  where q: "(q ∈ carrier P)" and
      f: "f = (monom P 1🪙R🪙 1 ⊖🪙 P🪙 monom P a 0) ⊗🪙P🪙 q ⊕🪙P🪙 monom P (eval R R id a f) 0"
     using remainder_theorem[OF Suc.prems(1) a_carrier R_not_triv] by auto
    hence lin_fac: "f = (monom P 1🪙R🪙 1 ⊖🪙 P🪙 monom P a 0) ⊗🪙P🪙 q" using q by (simp add: a_root)
    have deg: "deg R (monom P 1🪙R🪙 1 ⊖🪙 P🪙 monom P a 0) = 1"
      using a_carrier by (simp add: deg_minus_eq)
    hence mon_not_zero: "(monom P 1🪙R🪙 1 ⊖🪙 P🪙 monom P a 0) ≠ 0🪙P🪙"
      by (fastforce simp del: r_right_minus_eq)
    have q_not_zero: "q ≠ 0🪙P🪙" using Suc by (auto simp add : lin_fac)
    hence "deg R q = x" using Suc deg deg_mult[OF mon_not_zero q_not_zero _ q]
      by (simp add : lin_fac)
    hence q_IH: "finite {a ∈ carrier R . eval R R id a q = 0}
                ∧ card {a ∈ carrier R . eval R R id a q = 0} ≤ x" using Suc q q_not_zero by blast
    have subs: "{a ∈ carrier R . eval R R id a f = 0}
                ⊆ {a ∈ carrier R . eval R R id a q = 0} ∪ {a}" (is "?L ⊆ ?R ∪ {a}")
      using a_carrier ‹q ∈ _›
      by (auto simp: evalRR_simps lin_fac R.integral_iff)
    have "{a ∈ carrier R . eval R R id a f = 0} ⊆ insert a {a ∈ carrier R . eval R R id a q = 0}"
     using subs by auto
    hence "card {a ∈ carrier R . eval R R id a f = 0} ≤
           card (insert a {a ∈ carrier R . eval R R id a q = 0})" using q_IH by (blast intro: card_mono)
    also have "… ≤ deg R f" using q_IH ‹Suc x = _›
      by (simp add: card_insert_if)
    finally show ?thesis using q_IH ‹Suc x = _› using finite by force
  next
    case False
    hence "card {a ∈ carrier R. eval R R id a f = 0} = 0" using finite by auto
    also have "… ≤ deg R f" by simp
    finally show ?thesis using finite by auto
  qed
qed

end

lemma (in domain) num_roots_le_deg :
  fixes p d :: nat
  assumes finite: "finite (carrier R)"
  assumes d_neq_zero: "d ≠ 0"
  shows "card {x ∈ carrier R. x [^] d = 1} ≤ d"
proof -
  let ?f = "monom (UP R) 1🪙R🪙 d ⊖🪙 (UP R)🪙 monom (UP R) 1🪙R🪙 0"
  have one_in_carrier: "1 ∈ carrier R" by simp
  interpret R: UP_domain R "UP R" by (unfold_locales)
  have "deg R ?f = d"
    using d_neq_zero by (simp add: R.deg_minus_eq)
  hence f_not_zero: "?f ≠ 0🪙UP R🪙" using  d_neq_zero by (auto simp add : R.deg_nzero_nzero)
  have roots_bound: "finite {a ∈ carrier R . eval R R id a ?f = 0} ∧
                    card {a ∈ carrier R . eval R R id a ?f = 0} ≤ deg R ?f"
                    using finite by (intro R.roots_bound[OF _ f_not_zero]) simp
  have subs: "{x ∈ carrier R. x [^] d = 1} ⊆ {a ∈ carrier R . eval R R id a ?f = 0}"
    by (auto simp: R.evalRR_simps)
  then have "card {x ∈ carrier R. x [^] d = 1} ≤
        card {a ∈ carrier R. eval R R id a ?f = 0}" using finite by (simp add : card_mono)
  thus ?thesis using ‹deg R ?f = d› roots_bound by linarith
qed



section ‹The Multiplicative Group of a Field›
text_raw ‹\label{sec:mult-group}›


text ‹
  In this section we show that the multiplicative group of a finite field
  is generated by a single element, i.e. it is cyclic. The proof is inspired
  by the first proof given in the survey~🍋‹"conrad-cyclicity"›.
 ›

context field begin

lemma num_elems_of_ord_eq_phi':
  assumes finite: "finite (carrier R)" and dvd: "d dvd order (mult_of R)"
      and exists: "∃a∈carrier (mult_of R). group.ord (mult_of R) a = d"
  shows "card {a ∈ carrier (mult_of R). group.ord (mult_of R) a = d} = phi' d"
proof -
  note mult_of_simps[simp]
  have finite': "finite (carrier (mult_of R))" using finite by (rule finite_mult_of)

  interpret G:group "mult_of R" rewrites "([^]🪙mult_of R🪙) = (([^]) :: _ ==> nat ==> _)" and "1🪙mult_of R🪙 = 1"
    by (rule field_mult_group) simp_all

  from exists
  obtain a where a: "a ∈ carrier (mult_of R)" and ord_a: "group.ord (mult_of R) a = d"
    by (auto simp add: card_gt_0_iff)

  have set_eq1: "{a[^]n| n. n ∈ {1 .. d}} = {x ∈ carrier (mult_of R). x [^] d = 1}"
  proof (rule card_seteq)
    show "finite {x ∈ carrier (mult_of R). x [^] d = 1}" using finite by auto

    show "{a[^]n| n. n ∈ {1 ..d}} ⊆ {x ∈ carrier (mult_of R). x[^]d = 1}"
    proof
      fix x assume "x ∈ {a[^]n | n. n ∈ {1 .. d}}"
      then obtain n where n: "x = a[^]n ∧ n ∈ {1 .. d}" by auto
      have "x[^]d =(a[^]d)[^]n" using n a ord_a by (simp add:nat_pow_pow mult.commute)
      hence "x[^]d = 1" using ord_a G.pow_ord_eq_1[OF a] by fastforce
      thus "x ∈ {x ∈ carrier (mult_of R). x[^]d = 1}" using G.nat_pow_closed[OF a] n by blast
    qed

    show "card {x ∈ carrier (mult_of R). x [^] d = 1} ≤ card {a[^]n | n. n ∈ {1 .. d}}"
    proof -
      have *: "{a[^]n | n. n ∈ {1 .. d }} = ((λ n. a[^]n) ` {1 .. d})" by auto
      have "0 < order (mult_of R)" unfolding order_mult_of[OF finite]
        using card_mono[OF finite, of "{0, 1}"] by (simp add: order_def)
      have "card {x ∈ carrier (mult_of R). x [^] d = 1} ≤ card {x ∈ carrier R. x [^] d = 1}"
        using finite by (auto intro: card_mono)
      also have "… ≤ d" using ‹0 🚫 (mult_of R)› num_roots_le_deg[OF finite, of d]
        by (simp add : dvd_pos_nat[OF _ ‹d dvd order (mult_of R)›])
      finally show ?thesis using G.ord_inj'[OF a] ord_a * by (simp add: card_image)
    qed
  qed

  have set_eq2: "{x ∈ carrier (mult_of R) . group.ord (mult_of R) x = d}
                = (λ n . a[^]n) ` {n ∈ {1 .. d}. group.ord (mult_of R) (a[^]n) = d}" (is "?L = ?R")
  proof
    have "x ∈ ?R" if x: "x ∈ (carrier (mult_of R)) ∧ group.ord (mult_of R) x = d" for x
    proof -
      from that have "x ∈ {x ∈ carrier (mult_of R). x [^] d = 1}"
        by (simp add: G.pow_ord_eq_1[of x, symmetric])
      then obtain n where n: "x = a[^]n ∧ n ∈ {1 .. d}" using set_eq1 by blast
      then show ?thesis using x by fast
    qed
    thus "?L ⊆ ?R" by blast
    show "?R ⊆ ?L" using a by (auto simp add: carrier_mult_of[symmetric] simp del: carrier_mult_of)
  qed
  have "inj_on (λ n . a[^]n) {n ∈ {1 .. d}. group.ord (mult_of R) (a[^]n) = d}"
    using G.ord_inj'[OF a, unfolded ord_a] unfolding inj_on_def by fast
  hence "card ((λn. a[^]n) ` {n ∈ {1 .. d}. group.ord (mult_of R) (a[^]n) = d})
         = card {k ∈ {1 .. d}. group.ord (mult_of R) (a[^]k) = d}"
         using card_image by blast
  thus ?thesis using set_eq2 G.pow_ord_eq_ord_iff[OF finite' ‹a ∈ _›, unfolded ord_a]
    by (simp add: phi'_def)
qed

end


theorem (in field) finite_field_mult_group_has_gen :
  assumes finite: "finite (carrier R)"
  shows "∃ a ∈ carrier (mult_of R) . carrier (mult_of R) = {a[^]i | i::nat . i ∈ UNIV}"
proof -
  note mult_of_simps[simp]
  have finite': "finite (carrier (mult_of R))" using finite by (rule finite_mult_of)

  interpret G: group "mult_of R" rewrites
      "([^]🪙mult_of R🪙) = (([^]) :: _ ==> nat ==> _)" and "1🪙mult_of R🪙 = 1"
    by (rule field_mult_group) (simp_all add: fun_eq_iff nat_pow_def)

  let ?N = "λ x . card {a ∈ carrier (mult_of R). group.ord (mult_of R) a = x}"
  have "0 < order R - 1" unfolding order_def using card_mono[OF finite, of "{0, 1}"] by simp
  then have *: "0 < order (mult_of R)" using assms by (simp add: order_mult_of)
  have fin: "finite {d. d dvd order (mult_of R) }" using dvd_nat_bounds[OF *] by force

  have "(∑d | d dvd order (mult_of R). ?N d)
      = card (UN d:{d . d dvd order (mult_of R) }. {a ∈ carrier (mult_of R). group.ord (mult_of R) a = d})"
      (is "_ = card ?U")
    using fin finite by (subst card_UN_disjoint) auto
  also have "?U = carrier (mult_of R)"
  proof
    have "x ∈ ?U" if x: "x ∈ carrier (mult_of R)" for x
    proof -
      from that have x': "x∈carrier (mult_of R)" by simp
      then have "group.ord (mult_of R) x dvd order (mult_of R)"
        using G.ord_dvd_group_order by blast
      then show ?thesis
        using dvd_nat_bounds[of "order (mult_of R)" "group.ord (mult_of R) x"] x by blast
    qed
    thus "carrier (mult_of R) ⊆ ?U" by blast
  qed auto
  also have "card ... = order (mult_of R)"
    using order_mult_of finite' by (simp add: order_def)
  finally have sum_Ns_eq: "(∑d | d dvd order (mult_of R). ?N d) = order (mult_of R)" .

  have "card {a ∈ carrier (mult_of R). group.ord (mult_of R) a = d} ≤ phi' d"
    if d: "d dvd order (mult_of R)" for d
  proof (cases "card {a ∈ carrier (mult_of R). group.ord (mult_of R) a = d} = 0")
    case True
    thus ?thesis by presburger
  next
    case False
    hence "∃a ∈ carrier (mult_of R). group.ord (mult_of R) a = d" by (auto simp: card_eq_0_iff)
    thus ?thesis using num_elems_of_ord_eq_phi'[OF finite d] by auto
  qed
  hence all_le: "∧i. i ∈ {d. d dvd order (mult_of R) }
        ==> (λi. card {a ∈ carrier (mult_of R). group.ord (mult_of R) a = i}) i ≤ (λi. phi' i) i" by fast
  hence le: "(∑i | i dvd order (mult_of R). ?N i)
            ≤ (∑i | i dvd order (mult_of R). phi' i)"
            using sum_mono[of "{d . d dvd order (mult_of R)}"
                  "λi. card {a ∈ carrier (mult_of R). group.ord (mult_of R) a = i}"] by presburger
  have "order (mult_of R) = (∑d | d dvd order (mult_of R). phi' d)" using *
    by (simp add: sum_phi'_factors)
  hence eq: "(∑i | i dvd order (mult_of R). ?N i)
          = (∑i | i dvd order (mult_of R). phi' i)" using le sum_Ns_eq by presburger
  have "∧i. i ∈ {d. d dvd order (mult_of R) } ==> ?N i = (λi. phi' i) i"
  proof (rule ccontr)
    fix i
    assume i1: "i ∈ {d. d dvd order (mult_of R)}" and "?N i ≠ phi' i"
    hence "?N i = 0"
      using num_elems_of_ord_eq_phi'[OF finite, of i] by (auto simp: card_eq_0_iff)
    moreover  have "0 < i" using * i1 by (simp add: dvd_nat_bounds[of "order (mult_of R)" i])
    ultimately have "?N i < phi' i" using phi'_nonzero by presburger
    hence "(∑i | i dvd order (mult_of R). ?N i)
         < (∑i | i dvd order (mult_of R). phi' i)"
      using sum_strict_mono_ex1[OF fin, of "?N" "λ i . phi' i"]
            i1 all_le by auto
    thus False using eq by force
  qed
  hence "?N (order (mult_of R)) > 0" using * by (simp add: phi'_nonzero)
  then obtain a where a: "a ∈ carrier (mult_of R)" and a_ord: "group.ord (mult_of R) a = order (mult_of R)"
    by (auto simp add: card_gt_0_iff)
  hence set_eq: "{a[^]i | i::nat. i ∈ UNIV} = (λx. a[^]x) ` {0 .. group.ord (mult_of R) a - 1}"
    using G.ord_elems[OF finite'] by auto
  have card_eq: "card ((λx. a[^]x) ` {0 .. group.ord (mult_of R) a - 1}) = card {0 .. group.ord (mult_of R) a - 1}"
    by (intro card_image G.ord_inj finite' a)
  hence "card ((λ x . a[^]x) ` {0 .. group.ord (mult_of R) a - 1}) = card {0 ..order (mult_of R) - 1}"
    using assms by (simp add: card_eq a_ord)
  hence card_R_minus_1: "card {a[^]i | i::nat. i ∈ UNIV} = order (mult_of R)"
    using * by (subst set_eq) auto
  have **: "{a[^]i | i::nat. i ∈ UNIV} ⊆ carrier (mult_of R)"
    using G.nat_pow_closed[OF a] by auto
  with _ have "carrier (mult_of R) = {a[^]i|i::nat. i ∈ UNIV}"
    by (rule card_seteq[symmetric]) (simp_all add: card_R_minus_1 finite order_def del: UNIV_I)
  thus ?thesis using a by blast
qed

end