src/HOL/Algebra/Multiplicative_Group.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 66500 ba94aeb02fbc
child 67051 e7e54a0b9197
permissions -rw-r--r--
more robust sorted_entries;
haftmann@65416
     1
(*  Title:      HOL/Algebra/Multiplicative_Group.thy
haftmann@65416
     2
    Author:     Simon Wimmer
haftmann@65416
     3
    Author:     Lars Noschinski
haftmann@65416
     4
*)
haftmann@65416
     5
haftmann@65416
     6
theory Multiplicative_Group
haftmann@65416
     7
imports
haftmann@65416
     8
  Complex_Main
haftmann@65416
     9
  Group
haftmann@65416
    10
  More_Group
haftmann@65416
    11
  More_Finite_Product
haftmann@65416
    12
  Coset
haftmann@65416
    13
  UnivPoly
haftmann@65416
    14
begin
haftmann@65416
    15
haftmann@65416
    16
section {* Simplification Rules for Polynomials *}
haftmann@65416
    17
text_raw {* \label{sec:simp-rules} *}
haftmann@65416
    18
haftmann@65416
    19
lemma (in ring_hom_cring) hom_sub[simp]:
haftmann@65416
    20
  assumes "x \<in> carrier R" "y \<in> carrier R"
haftmann@65416
    21
  shows "h (x \<ominus> y) = h x \<ominus>\<^bsub>S\<^esub> h y"
haftmann@65416
    22
  using assms by (simp add: R.minus_eq S.minus_eq)
haftmann@65416
    23
haftmann@65416
    24
context UP_ring begin
haftmann@65416
    25
haftmann@65416
    26
lemma deg_nzero_nzero:
haftmann@65416
    27
  assumes deg_p_nzero: "deg R p \<noteq> 0"
haftmann@65416
    28
  shows "p \<noteq> \<zero>\<^bsub>P\<^esub>"
haftmann@65416
    29
  using deg_zero deg_p_nzero by auto
haftmann@65416
    30
haftmann@65416
    31
lemma deg_add_eq:
haftmann@65416
    32
  assumes c: "p \<in> carrier P" "q \<in> carrier P"
haftmann@65416
    33
  assumes "deg R q \<noteq> deg R p"
haftmann@65416
    34
  shows "deg R (p \<oplus>\<^bsub>P\<^esub> q) = max (deg R p) (deg R q)"
haftmann@65416
    35
proof -
haftmann@65416
    36
  let ?m = "max (deg R p) (deg R q)"
haftmann@65416
    37
  from assms have "coeff P p ?m = \<zero> \<longleftrightarrow> coeff P q ?m \<noteq> \<zero>"
haftmann@65416
    38
    by (metis deg_belowI lcoeff_nonzero[OF deg_nzero_nzero] linear max.absorb_iff2 max.absorb1)
haftmann@65416
    39
  then have "coeff P (p \<oplus>\<^bsub>P\<^esub> q) ?m \<noteq> \<zero>"
haftmann@65416
    40
    using assms by auto
haftmann@65416
    41
  then have "deg R (p \<oplus>\<^bsub>P\<^esub> q) \<ge> ?m"
haftmann@65416
    42
    using assms by (blast intro: deg_belowI)
haftmann@65416
    43
  with deg_add[OF c] show ?thesis by arith
haftmann@65416
    44
qed
haftmann@65416
    45
haftmann@65416
    46
lemma deg_minus_eq:
haftmann@65416
    47
  assumes "p \<in> carrier P" "q \<in> carrier P" "deg R q \<noteq> deg R p"
haftmann@65416
    48
  shows "deg R (p \<ominus>\<^bsub>P\<^esub> q) = max (deg R p) (deg R q)"
haftmann@65416
    49
  using assms by (simp add: deg_add_eq a_minus_def)
haftmann@65416
    50
haftmann@65416
    51
end
haftmann@65416
    52
haftmann@65416
    53
context UP_cring begin
haftmann@65416
    54
haftmann@65416
    55
lemma evalRR_add:
haftmann@65416
    56
  assumes "p \<in> carrier P" "q \<in> carrier P"
haftmann@65416
    57
  assumes x:"x \<in> carrier R"
haftmann@65416
    58
  shows "eval R R id x (p \<oplus>\<^bsub>P\<^esub> q) = eval R R id x p \<oplus> eval R R id x q"
haftmann@65416
    59
proof -
haftmann@65416
    60
  interpret UP_pre_univ_prop R R id by unfold_locales simp
haftmann@65416
    61
  interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
haftmann@65416
    62
  show ?thesis using assms by simp
haftmann@65416
    63
qed
haftmann@65416
    64
haftmann@65416
    65
lemma evalRR_sub:
haftmann@65416
    66
  assumes "p \<in> carrier P" "q \<in> carrier P"
haftmann@65416
    67
  assumes x:"x \<in> carrier R"
haftmann@65416
    68
  shows "eval R R id x (p \<ominus>\<^bsub>P\<^esub> q) = eval R R id x p \<ominus> eval R R id x q"
haftmann@65416
    69
proof -
haftmann@65416
    70
  interpret UP_pre_univ_prop R R id by unfold_locales simp
haftmann@65416
    71
  interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
haftmann@65416
    72
  show ?thesis using assms by simp
haftmann@65416
    73
qed
haftmann@65416
    74
haftmann@65416
    75
lemma evalRR_mult:
haftmann@65416
    76
  assumes "p \<in> carrier P" "q \<in> carrier P"
haftmann@65416
    77
  assumes x:"x \<in> carrier R"
haftmann@65416
    78
  shows "eval R R id x (p \<otimes>\<^bsub>P\<^esub> q) = eval R R id x p \<otimes> eval R R id x q"
haftmann@65416
    79
proof -
haftmann@65416
    80
  interpret UP_pre_univ_prop R R id by unfold_locales simp
haftmann@65416
    81
  interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
haftmann@65416
    82
  show ?thesis using assms by simp
haftmann@65416
    83
qed
haftmann@65416
    84
haftmann@65416
    85
lemma evalRR_monom:
haftmann@65416
    86
  assumes a: "a \<in> carrier R" and x: "x \<in> carrier R"
haftmann@65416
    87
  shows "eval R R id x (monom P a d) = a \<otimes> x (^) d"
haftmann@65416
    88
proof -
haftmann@65416
    89
  interpret UP_pre_univ_prop R R id by unfold_locales simp
haftmann@65416
    90
  show ?thesis using assms by (simp add: eval_monom)
haftmann@65416
    91
qed
haftmann@65416
    92
haftmann@65416
    93
lemma evalRR_one:
haftmann@65416
    94
  assumes x: "x \<in> carrier R"
haftmann@65416
    95
  shows "eval R R id x \<one>\<^bsub>P\<^esub> = \<one>"
haftmann@65416
    96
proof -
haftmann@65416
    97
  interpret UP_pre_univ_prop R R id by unfold_locales simp
haftmann@65416
    98
  interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
haftmann@65416
    99
  show ?thesis using assms by simp
haftmann@65416
   100
qed
haftmann@65416
   101
haftmann@65416
   102
lemma carrier_evalRR:
haftmann@65416
   103
  assumes x: "x \<in> carrier R" and "p \<in> carrier P"
haftmann@65416
   104
  shows "eval R R id x p \<in> carrier R"
haftmann@65416
   105
proof -
haftmann@65416
   106
  interpret UP_pre_univ_prop R R id by unfold_locales simp
haftmann@65416
   107
  interpret ring_hom_cring P R "eval R R id x" by unfold_locales (rule eval_ring_hom[OF x])
haftmann@65416
   108
  show ?thesis using assms by simp
haftmann@65416
   109
qed
haftmann@65416
   110
haftmann@65416
   111
lemmas evalRR_simps = evalRR_add evalRR_sub evalRR_mult evalRR_monom evalRR_one carrier_evalRR
haftmann@65416
   112
haftmann@65416
   113
end
haftmann@65416
   114
haftmann@65416
   115
haftmann@65416
   116
haftmann@65416
   117
section {* Properties of the Euler @{text \<phi>}-function *}
haftmann@65416
   118
text_raw {* \label{sec:euler-phi} *}
haftmann@65416
   119
haftmann@65416
   120
text{*
haftmann@65416
   121
  In this section we prove that for every positive natural number the equation
haftmann@65416
   122
  $\sum_{d | n}^n \varphi(d) = n$ holds.
haftmann@65416
   123
*}
haftmann@65416
   124
haftmann@65416
   125
lemma dvd_div_ge_1 :
haftmann@65416
   126
  fixes a b :: nat
haftmann@65416
   127
  assumes "a \<ge> 1" "b dvd a"
haftmann@65416
   128
  shows "a div b \<ge> 1"
haftmann@65416
   129
proof -
haftmann@65416
   130
  from \<open>b dvd a\<close> obtain c where "a = b * c" ..
haftmann@65416
   131
  with \<open>a \<ge> 1\<close> show ?thesis by simp
haftmann@65416
   132
qed
haftmann@65416
   133
haftmann@65416
   134
lemma dvd_nat_bounds :
haftmann@65416
   135
 fixes n p :: nat
haftmann@65416
   136
 assumes "p > 0" "n dvd p"
haftmann@65416
   137
 shows "n > 0 \<and> n \<le> p"
haftmann@65416
   138
 using assms by (simp add: dvd_pos_nat dvd_imp_le)
haftmann@65416
   139
haftmann@65416
   140
(* Deviates from the definition given in the library in number theory *)
haftmann@65416
   141
definition phi' :: "nat => nat"
haftmann@65416
   142
  where "phi' m = card {x. 1 \<le> x \<and> x \<le> m \<and> gcd x m = 1}"
haftmann@65416
   143
haftmann@66500
   144
notation (latex output)
haftmann@65416
   145
  phi' ("\<phi> _")
haftmann@65416
   146
haftmann@65416
   147
lemma phi'_nonzero :
haftmann@65416
   148
  assumes "m > 0"
haftmann@65416
   149
  shows "phi' m > 0"
haftmann@65416
   150
proof -
haftmann@65416
   151
  have "1 \<in> {x. 1 \<le> x \<and> x \<le> m \<and> gcd x m = 1}" using assms by simp
haftmann@65416
   152
  hence "card {x. 1 \<le> x \<and> x \<le> m \<and> gcd x m = 1} > 0" by (auto simp: card_gt_0_iff)
haftmann@65416
   153
  thus ?thesis unfolding phi'_def by simp
haftmann@65416
   154
qed
haftmann@65416
   155
haftmann@65416
   156
lemma dvd_div_eq_1:
haftmann@65416
   157
  fixes a b c :: nat
haftmann@65416
   158
  assumes "c dvd a" "c dvd b" "a div c = b div c"
haftmann@65416
   159
  shows "a = b" using assms dvd_mult_div_cancel[OF `c dvd a`] dvd_mult_div_cancel[OF `c dvd b`]
haftmann@65416
   160
                by presburger
haftmann@65416
   161
haftmann@65416
   162
lemma dvd_div_eq_2:
haftmann@65416
   163
  fixes a b c :: nat
haftmann@65416
   164
  assumes "c>0" "a dvd c" "b dvd c" "c div a = c div b"
haftmann@65416
   165
  shows "a = b"
haftmann@65416
   166
  proof -
haftmann@65416
   167
  have "a > 0" "a \<le> c" using dvd_nat_bounds[OF assms(1-2)] by auto
haftmann@65416
   168
  have "a*(c div a) = c" using assms dvd_mult_div_cancel by fastforce
haftmann@65416
   169
  also have "\<dots> = b*(c div a)" using assms dvd_mult_div_cancel by fastforce
haftmann@65416
   170
  finally show "a = b" using `c>0` dvd_div_ge_1[OF _ `a dvd c`] by fastforce
haftmann@65416
   171
qed
haftmann@65416
   172
haftmann@65416
   173
lemma div_mult_mono:
haftmann@65416
   174
  fixes a b c :: nat
haftmann@65416
   175
  assumes "a > 0" "a\<le>d"
haftmann@65416
   176
  shows "a * b div d \<le> b"
haftmann@65416
   177
proof -
haftmann@65416
   178
  have "a*b div d \<le> b*a div a" using assms div_le_mono2 mult.commute[of a b] by presburger
haftmann@65416
   179
  thus ?thesis using assms by force
haftmann@65416
   180
qed
haftmann@65416
   181
haftmann@65416
   182
text{*
haftmann@65416
   183
  We arrive at the main result of this section:
haftmann@65416
   184
  For every positive natural number the equation $\sum_{d | n}^n \varphi(d) = n$ holds.
haftmann@65416
   185
haftmann@65416
   186
  The outline of the proof for this lemma is as follows:
haftmann@65416
   187
  We count the $n$ fractions $1/n$, $\ldots$, $(n-1)/n$, $n/n$.
haftmann@65416
   188
  We analyze the reduced form $a/d = m/n$ for any of those fractions.
haftmann@65416
   189
  We want to know how many fractions $m/n$ have the reduced form denominator $d$.
haftmann@65416
   190
  The condition $1 \leq m \leq n$ is equivalent to the condition $1 \leq a \leq d$.
haftmann@65416
   191
  Therefore we want to know how many $a$ with $1 \leq a \leq d$ exist, s.t. @{term "gcd a d = 1"}.
haftmann@65416
   192
  This number is exactly @{term "phi' d"}.
haftmann@65416
   193
haftmann@65416
   194
  Finally, by counting the fractions $m/n$ according to their reduced form denominator,
haftmann@65416
   195
  we get: @{term [display] "(\<Sum>d | d dvd n . phi' d) = n"}.
haftmann@65416
   196
  To formalize this proof in Isabelle, we analyze for an arbitrary divisor $d$ of $n$
haftmann@65416
   197
  \begin{itemize}
haftmann@65416
   198
    \item the set of reduced form numerators @{term "{a. (1::nat) \<le> a \<and> a \<le> d \<and> coprime a d}"}
haftmann@65416
   199
    \item the set of numerators $m$, for which $m/n$ has the reduced form denominator $d$,
haftmann@65416
   200
      i.e. the set @{term "{m \<in> {1::nat .. n}. n div gcd m n = d}"}
haftmann@65416
   201
  \end{itemize}
haftmann@65416
   202
  We show that @{term "\<lambda>a. a*n div d"} with the inverse @{term "\<lambda>a. a div gcd a n"} is
haftmann@65416
   203
  a bijection between theses sets, thus yielding the equality
haftmann@65416
   204
  @{term [display] "phi' d = card {m \<in> {1 .. n}. n div gcd m n = d}"}
haftmann@65416
   205
  This gives us
haftmann@65416
   206
  @{term [display] "(\<Sum>d | d dvd n . phi' d)
haftmann@65416
   207
          = card (\<Union>d \<in> {d. d dvd n}. {m \<in> {1 .. n}. n div gcd m n = d})"}
haftmann@65416
   208
  and by showing
haftmann@65416
   209
  @{term "(\<Union>d \<in> {d. d dvd n}. {m \<in> {1::nat .. n}. n div gcd m n = d}) \<supseteq> {1 .. n}"}
haftmann@65416
   210
  (this is our counting argument) the thesis follows.
haftmann@65416
   211
*}
haftmann@65416
   212
lemma sum_phi'_factors :
haftmann@65416
   213
 fixes n :: nat
haftmann@65416
   214
 assumes "n > 0"
haftmann@65416
   215
 shows "(\<Sum>d | d dvd n. phi' d) = n"
haftmann@65416
   216
proof -
haftmann@65416
   217
  { fix d assume "d dvd n" then obtain q where q: "n = d * q" ..
haftmann@65416
   218
    have "card {a. 1 \<le> a \<and> a \<le> d \<and> coprime a d} = card {m \<in> {1 .. n}.  n div gcd m n = d}"
haftmann@65416
   219
         (is "card ?RF = card ?F")
haftmann@65416
   220
    proof (rule card_bij_eq)
haftmann@65416
   221
      { fix a b assume "a * n div d = b * n div d"
haftmann@65416
   222
        hence "a * (n div d) = b * (n div d)"
haftmann@65416
   223
          using dvd_div_mult[OF `d dvd n`] by (fastforce simp add: mult.commute)
haftmann@65416
   224
        hence "a = b" using dvd_div_ge_1[OF _ `d dvd n`] `n>0`
haftmann@65416
   225
          by (simp add: mult.commute nat_mult_eq_cancel1)
haftmann@65416
   226
      } thus "inj_on (\<lambda>a. a*n div d) ?RF" unfolding inj_on_def by blast
haftmann@65416
   227
      { fix a assume a:"a\<in>?RF"
haftmann@65416
   228
        hence "a * (n div d) \<ge> 1" using `n>0` dvd_div_ge_1[OF _ `d dvd n`] by simp
haftmann@65416
   229
        hence ge_1:"a * n div d \<ge> 1" by (simp add: `d dvd n` div_mult_swap)
haftmann@65416
   230
        have le_n:"a * n div d \<le> n" using div_mult_mono a by simp
haftmann@65416
   231
        have "gcd (a * n div d) n = n div d * gcd a d"
haftmann@65416
   232
          by (simp add: gcd_mult_distrib_nat q ac_simps)
haftmann@65416
   233
        hence "n div gcd (a * n div d) n = d*n div (d*(n div d))" using a by simp
haftmann@65416
   234
        hence "a * n div d \<in> ?F"
haftmann@65416
   235
          using ge_1 le_n by (fastforce simp add: `d dvd n` dvd_mult_div_cancel)
haftmann@65416
   236
      } thus "(\<lambda>a. a*n div d) ` ?RF \<subseteq> ?F" by blast
haftmann@65416
   237
      { fix m l assume A: "m \<in> ?F" "l \<in> ?F" "m div gcd m n = l div gcd l n"
haftmann@65416
   238
        hence "gcd m n = gcd l n" using dvd_div_eq_2[OF assms] by fastforce
haftmann@65416
   239
        hence "m = l" using dvd_div_eq_1[of "gcd m n" m l] A(3) by fastforce
haftmann@65416
   240
      } thus "inj_on (\<lambda>a. a div gcd a n) ?F" unfolding inj_on_def by blast
haftmann@65416
   241
      { fix m assume "m \<in> ?F"
haftmann@65416
   242
        hence "m div gcd m n \<in> ?RF" using dvd_div_ge_1
haftmann@65416
   243
          by (fastforce simp add: div_le_mono div_gcd_coprime)
haftmann@65416
   244
      } thus "(\<lambda>a. a div gcd a n) ` ?F \<subseteq> ?RF" by blast
haftmann@65416
   245
    qed force+
haftmann@65416
   246
  } hence phi'_eq:"\<And>d. d dvd n \<Longrightarrow> phi' d = card {m \<in> {1 .. n}. n div gcd m n = d}"
haftmann@65416
   247
      unfolding phi'_def by presburger
haftmann@65416
   248
  have fin:"finite {d. d dvd n}" using dvd_nat_bounds[OF `n>0`] by force
haftmann@65416
   249
  have "(\<Sum>d | d dvd n. phi' d)
haftmann@65416
   250
                 = card (\<Union>d \<in> {d. d dvd n}. {m \<in> {1 .. n}. n div gcd m n = d})"
haftmann@65416
   251
    using card_UN_disjoint[OF fin, of "(\<lambda>d. {m \<in> {1 .. n}. n div gcd m n = d})"] phi'_eq
haftmann@65416
   252
    by fastforce
haftmann@65416
   253
  also have "(\<Union>d \<in> {d. d dvd n}. {m \<in> {1 .. n}. n div gcd m n = d}) = {1 .. n}" (is "?L = ?R")
haftmann@65416
   254
  proof
haftmann@65416
   255
    show "?L \<supseteq> ?R"
haftmann@65416
   256
    proof
haftmann@65416
   257
      fix m assume m: "m \<in> ?R"
haftmann@65416
   258
      thus "m \<in> ?L" using dvd_triv_right[of "n div gcd m n" "gcd m n"]
haftmann@65416
   259
        by (simp add: dvd_mult_div_cancel)
haftmann@65416
   260
    qed
haftmann@65416
   261
  qed fastforce
haftmann@65416
   262
  finally show ?thesis by force
haftmann@65416
   263
qed
haftmann@65416
   264
haftmann@65416
   265
section {* Order of an Element of a Group *}
haftmann@65416
   266
text_raw {* \label{sec:order-elem} *}
haftmann@65416
   267
haftmann@65416
   268
haftmann@65416
   269
context group begin
haftmann@65416
   270
haftmann@65416
   271
lemma pow_eq_div2 :
haftmann@65416
   272
  fixes m n :: nat
haftmann@65416
   273
  assumes x_car: "x \<in> carrier G"
haftmann@65416
   274
  assumes pow_eq: "x (^) m = x (^) n"
haftmann@65416
   275
  shows "x (^) (m - n) = \<one>"
haftmann@65416
   276
proof (cases "m < n")
haftmann@65416
   277
  case False
haftmann@65416
   278
  have "\<one> \<otimes> x (^) m = x (^) m" by (simp add: x_car)
haftmann@65416
   279
  also have "\<dots> = x (^) (m - n) \<otimes> x (^) n"
haftmann@65416
   280
    using False by (simp add: nat_pow_mult x_car)
haftmann@65416
   281
  also have "\<dots> = x (^) (m - n) \<otimes> x (^) m"
haftmann@65416
   282
    by (simp add: pow_eq)
haftmann@65416
   283
  finally show ?thesis by (simp add: x_car)
haftmann@65416
   284
qed simp
haftmann@65416
   285
haftmann@65416
   286
definition ord where "ord a = Min {d \<in> {1 .. order G} . a (^) d = \<one>}"
haftmann@65416
   287
haftmann@65416
   288
lemma
haftmann@65416
   289
  assumes finite:"finite (carrier G)"
haftmann@65416
   290
  assumes a:"a \<in> carrier G"
haftmann@65416
   291
  shows ord_ge_1: "1 \<le> ord a" and ord_le_group_order: "ord a \<le> order G"
haftmann@65416
   292
    and pow_ord_eq_1: "a (^) ord a = \<one>"
haftmann@65416
   293
proof -
haftmann@65416
   294
  have "\<not>inj_on (\<lambda>x. a (^) x) {0 .. order G}"
haftmann@65416
   295
  proof (rule notI)
haftmann@65416
   296
    assume A: "inj_on (\<lambda>x. a (^) x) {0 .. order G}"
haftmann@65416
   297
    have "order G + 1 = card {0 .. order G}" by simp
haftmann@65416
   298
    also have "\<dots> = card ((\<lambda>x. a (^) x) ` {0 .. order G})" (is "_ = card ?S")
haftmann@65416
   299
      using A by (simp add: card_image)
haftmann@65416
   300
    also have "?S = {a (^) x | x. x \<in> {0 .. order G}}" by blast
haftmann@65416
   301
    also have "\<dots> \<subseteq> carrier G" (is "?S \<subseteq> _") using a by blast
haftmann@65416
   302
    then have "card ?S \<le> order G" unfolding order_def
haftmann@65416
   303
      by (rule card_mono[OF finite])
haftmann@65416
   304
    finally show False by arith
haftmann@65416
   305
  qed
haftmann@65416
   306
haftmann@65416
   307
  then obtain x y where x_y:"x \<noteq> y" "x \<in> {0 .. order G}" "y \<in> {0 .. order G}"
haftmann@65416
   308
                        "a (^) x = a (^) y" unfolding inj_on_def by blast
haftmann@65416
   309
  obtain d where "1 \<le> d" "a (^) d = \<one>" "d \<le> order G"
haftmann@65416
   310
  proof cases
haftmann@65416
   311
    assume "y < x" with x_y show ?thesis
haftmann@65416
   312
      by (intro that[where d="x - y"]) (auto simp add: pow_eq_div2[OF a])
haftmann@65416
   313
  next
haftmann@65416
   314
    assume "\<not>y < x" with x_y show ?thesis
haftmann@65416
   315
      by (intro that[where d="y - x"]) (auto simp add: pow_eq_div2[OF a])
haftmann@65416
   316
  qed
haftmann@65416
   317
  hence "ord a \<in> {d \<in> {1 .. order G} . a (^) d = \<one>}"
haftmann@65416
   318
    unfolding ord_def using Min_in[of "{d \<in> {1 .. order G} . a (^) d = \<one>}"]
haftmann@65416
   319
    by fastforce
haftmann@65416
   320
  then show "1 \<le> ord a" and "ord a \<le> order G" and "a (^) ord a = \<one>"
haftmann@65416
   321
    by (auto simp: order_def)
haftmann@65416
   322
qed
haftmann@65416
   323
haftmann@65416
   324
lemma finite_group_elem_finite_ord :
haftmann@65416
   325
  assumes "finite (carrier G)" "x \<in> carrier G"
haftmann@65416
   326
  shows "\<exists> d::nat. d \<ge> 1 \<and> x (^) d = \<one>"
haftmann@65416
   327
  using assms ord_ge_1 pow_ord_eq_1 by auto
haftmann@65416
   328
haftmann@65416
   329
lemma ord_min:
haftmann@65416
   330
  assumes  "finite (carrier G)" "1 \<le> d" "a \<in> carrier G" "a (^) d = \<one>" shows "ord a \<le> d"
haftmann@65416
   331
proof -
haftmann@65416
   332
  def Ord \<equiv> "{d \<in> {1..order G}. a (^) d = \<one>}"
haftmann@65416
   333
  have fin: "finite Ord" by (auto simp: Ord_def)
haftmann@65416
   334
  have in_ord: "ord a \<in> Ord"
haftmann@65416
   335
    using assms pow_ord_eq_1 ord_ge_1 ord_le_group_order by (auto simp: Ord_def)
haftmann@65416
   336
  then have "Ord \<noteq> {}" by auto
haftmann@65416
   337
haftmann@65416
   338
  show ?thesis
haftmann@65416
   339
  proof (cases "d \<le> order G")
haftmann@65416
   340
    case True
haftmann@65416
   341
    then have "d \<in> Ord" using assms by (auto simp: Ord_def)
haftmann@65416
   342
    with fin in_ord show ?thesis
haftmann@65416
   343
      unfolding ord_def Ord_def[symmetric] by simp
haftmann@65416
   344
  next
haftmann@65416
   345
    case False
haftmann@65416
   346
    then show ?thesis using in_ord by (simp add: Ord_def)
haftmann@65416
   347
  qed
haftmann@65416
   348
qed
haftmann@65416
   349
haftmann@65416
   350
lemma ord_inj :
haftmann@65416
   351
  assumes finite: "finite (carrier G)"
haftmann@65416
   352
  assumes a: "a \<in> carrier G"
haftmann@65416
   353
  shows "inj_on (\<lambda> x . a (^) x) {0 .. ord a - 1}"
haftmann@65416
   354
proof (rule inj_onI, rule ccontr)
haftmann@65416
   355
  fix x y assume A: "x \<in> {0 .. ord a - 1}" "y \<in> {0 .. ord a - 1}" "a (^) x= a (^) y" "x \<noteq> y"
haftmann@65416
   356
haftmann@65416
   357
  have "finite {d \<in> {1..order G}. a (^) d = \<one>}" by auto
haftmann@65416
   358
haftmann@65416
   359
  { fix x y assume A: "x < y" "x \<in> {0 .. ord a - 1}" "y \<in> {0 .. ord a - 1}"
haftmann@65416
   360
        "a (^) x = a (^) y"
haftmann@65416
   361
    hence "y - x < ord a" by auto
haftmann@65416
   362
    also have "\<dots> \<le> order G" using assms by (simp add: ord_le_group_order)
haftmann@65416
   363
    finally have y_x_range:"y - x \<in> {1 .. order G}" using A by force
haftmann@65416
   364
    have "a (^) (y-x) = \<one>" using a A by (simp add: pow_eq_div2)
haftmann@65416
   365
haftmann@65416
   366
    hence y_x:"y - x \<in> {d \<in> {1.. order G}. a (^) d = \<one>}" using y_x_range by blast
haftmann@65416
   367
    have "min (y - x) (ord a) = ord a"
haftmann@65416
   368
      using Min.in_idem[OF `finite {d \<in> {1 .. order G} . a (^) d = \<one>}` y_x] ord_def by auto
haftmann@65416
   369
    with `y - x < ord a` have False by linarith
haftmann@65416
   370
  }
haftmann@65416
   371
  note X = this
haftmann@65416
   372
haftmann@65416
   373
  { assume "x < y" with A X have False by blast }
haftmann@65416
   374
  moreover
haftmann@65416
   375
  { assume "x > y" with A X  have False by metis }
haftmann@65416
   376
  moreover
haftmann@65416
   377
  { assume "x = y" then have False using A by auto}
haftmann@65416
   378
  ultimately
haftmann@65416
   379
  show False by fastforce
haftmann@65416
   380
qed
haftmann@65416
   381
haftmann@65416
   382
lemma ord_inj' :
haftmann@65416
   383
  assumes finite: "finite (carrier G)"
haftmann@65416
   384
  assumes a: "a \<in> carrier G"
haftmann@65416
   385
  shows "inj_on (\<lambda> x . a (^) x) {1 .. ord a}"
haftmann@65416
   386
proof (rule inj_onI, rule ccontr)
haftmann@65416
   387
  fix x y :: nat
haftmann@65416
   388
  assume A:"x \<in> {1 .. ord a}" "y \<in> {1 .. ord a}" "a (^) x = a (^) y" "x\<noteq>y"
haftmann@65416
   389
  { assume "x < ord a" "y < ord a"
haftmann@65416
   390
    hence False using ord_inj[OF assms] A unfolding inj_on_def by fastforce
haftmann@65416
   391
  }
haftmann@65416
   392
  moreover
haftmann@65416
   393
  { assume "x = ord a" "y < ord a"
haftmann@65416
   394
    hence "a (^) y = a (^) (0::nat)" using pow_ord_eq_1[OF assms] A by auto
haftmann@65416
   395
    hence "y=0" using ord_inj[OF assms] `y < ord a` unfolding inj_on_def by force
haftmann@65416
   396
    hence False using A by fastforce
haftmann@65416
   397
  }
haftmann@65416
   398
  moreover
haftmann@65416
   399
  { assume "y = ord a" "x < ord a"
haftmann@65416
   400
    hence "a (^) x = a (^) (0::nat)" using pow_ord_eq_1[OF assms] A by auto
haftmann@65416
   401
    hence "x=0" using ord_inj[OF assms] `x < ord a` unfolding inj_on_def by force
haftmann@65416
   402
    hence False using A by fastforce
haftmann@65416
   403
  }
haftmann@65416
   404
  ultimately show False using A  by force
haftmann@65416
   405
qed
haftmann@65416
   406
haftmann@65416
   407
lemma ord_elems :
haftmann@65416
   408
  assumes "finite (carrier G)" "a \<in> carrier G"
haftmann@65416
   409
  shows "{a(^)x | x. x \<in> (UNIV :: nat set)} = {a(^)x | x. x \<in> {0 .. ord a - 1}}" (is "?L = ?R")
haftmann@65416
   410
proof
haftmann@65416
   411
  show "?R \<subseteq> ?L" by blast
haftmann@65416
   412
  { fix y assume "y \<in> ?L"
haftmann@65416
   413
    then obtain x::nat where x:"y = a(^)x" by auto
haftmann@65416
   414
    def r \<equiv> "x mod ord a"
haftmann@65416
   415
    then obtain q where q:"x = q * ord a + r" using mod_eqD by atomize_elim presburger
haftmann@65416
   416
    hence "y = (a(^)ord a)(^)q \<otimes> a(^)r"
haftmann@65416
   417
      using x assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
haftmann@65416
   418
    hence "y = a(^)r" using assms by (simp add: pow_ord_eq_1)
haftmann@65416
   419
    have "r < ord a" using ord_ge_1[OF assms] by (simp add: r_def)
haftmann@65416
   420
    hence "r \<in> {0 .. ord a - 1}" by (force simp: r_def)
haftmann@65416
   421
    hence "y \<in> {a(^)x | x. x \<in> {0 .. ord a - 1}}" using `y=a(^)r` by blast
haftmann@65416
   422
  }
haftmann@65416
   423
  thus "?L \<subseteq> ?R" by auto
haftmann@65416
   424
qed
haftmann@65416
   425
haftmann@65416
   426
lemma ord_dvd_pow_eq_1 :
haftmann@65416
   427
  assumes "finite (carrier G)" "a \<in> carrier G" "a (^) k = \<one>"
haftmann@65416
   428
  shows "ord a dvd k"
haftmann@65416
   429
proof -
haftmann@65416
   430
  def r \<equiv> "k mod ord a"
haftmann@65416
   431
  then obtain q where q:"k = q*ord a + r" using mod_eqD by atomize_elim presburger
haftmann@65416
   432
  hence "a(^)k = (a(^)ord a)(^)q \<otimes> a(^)r"
haftmann@65416
   433
      using assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
haftmann@65416
   434
  hence "a(^)k = a(^)r" using assms by (simp add: pow_ord_eq_1)
haftmann@65416
   435
  hence "a(^)r = \<one>" using assms(3) by simp
haftmann@65416
   436
  have "r < ord a" using ord_ge_1[OF assms(1-2)] by (simp add: r_def)
haftmann@65416
   437
  hence "r = 0" using `a(^)r = \<one>` ord_def[of a] ord_min[of r a] assms(1-2) by linarith
haftmann@65416
   438
  thus ?thesis using q by simp
haftmann@65416
   439
qed
haftmann@65416
   440
haftmann@65416
   441
lemma dvd_gcd :
haftmann@65416
   442
  fixes a b :: nat
haftmann@65416
   443
  obtains q where "a * (b div gcd a b) = b*q"
haftmann@65416
   444
proof
haftmann@65416
   445
  have "a * (b div gcd a b) = (a div gcd a b) * b" by (simp add:  div_mult_swap dvd_div_mult)
haftmann@65416
   446
  also have "\<dots> = b * (a div gcd a b)" by simp
haftmann@65416
   447
  finally show "a * (b div gcd a b) = b * (a div gcd a b) " .
haftmann@65416
   448
qed
haftmann@65416
   449
haftmann@65416
   450
lemma ord_pow_dvd_ord_elem :
haftmann@65416
   451
  assumes finite[simp]: "finite (carrier G)"
haftmann@65416
   452
  assumes a[simp]:"a \<in> carrier G"
haftmann@65416
   453
  shows "ord (a(^)n) = ord a div gcd n (ord a)"
haftmann@65416
   454
proof -
haftmann@65416
   455
  have "(a(^)n) (^) ord a = (a (^) ord a) (^) n"
haftmann@65416
   456
    by (simp add: mult.commute nat_pow_pow)
haftmann@65416
   457
  hence "(a(^)n) (^) ord a = \<one>" by (simp add: pow_ord_eq_1)
haftmann@65416
   458
  obtain q where "n * (ord a div gcd n (ord a)) = ord a * q" by (rule dvd_gcd)
haftmann@65416
   459
  hence "(a(^)n) (^) (ord a div gcd n (ord a)) = (a (^) ord a)(^)q"  by (simp add : nat_pow_pow)
haftmann@65416
   460
  hence pow_eq_1: "(a(^)n) (^) (ord a div gcd n (ord a)) = \<one>"
haftmann@65416
   461
     by (auto simp add : pow_ord_eq_1[of a])
haftmann@65416
   462
  have "ord a \<ge> 1" using ord_ge_1 by simp
haftmann@65416
   463
  have ge_1:"ord a div gcd n (ord a) \<ge> 1"
haftmann@65416
   464
  proof -
haftmann@65416
   465
    have "gcd n (ord a) dvd ord a" by blast
haftmann@65416
   466
    thus ?thesis by (rule dvd_div_ge_1[OF `ord a \<ge> 1`])
haftmann@65416
   467
  qed
haftmann@65416
   468
  have "ord a \<le> order G" by (simp add: ord_le_group_order)
haftmann@65416
   469
  have "ord a div gcd n (ord a) \<le> order G"
haftmann@65416
   470
  proof -
haftmann@65416
   471
    have "ord a div gcd n (ord a) \<le> ord a" by simp
haftmann@65416
   472
    thus ?thesis using `ord a \<le> order G` by linarith
haftmann@65416
   473
  qed
haftmann@65416
   474
  hence ord_gcd_elem:"ord a div gcd n (ord a) \<in> {d \<in> {1..order G}. (a(^)n) (^) d = \<one>}"
haftmann@65416
   475
    using ge_1 pow_eq_1 by force
haftmann@65416
   476
  { fix d :: nat
haftmann@65416
   477
    assume d_elem:"d \<in> {d \<in> {1..order G}. (a(^)n) (^) d = \<one>}"
haftmann@65416
   478
    assume d_lt:"d < ord a div gcd n (ord a)"
haftmann@65416
   479
    hence pow_nd:"a(^)(n*d)  = \<one>" using d_elem
haftmann@65416
   480
      by (simp add : nat_pow_pow)
haftmann@65416
   481
    hence "ord a dvd n*d" using assms by (auto simp add : ord_dvd_pow_eq_1)
haftmann@65416
   482
    then obtain q where "ord a * q = n*d" by (metis dvd_mult_div_cancel)
haftmann@65416
   483
    hence prod_eq:"(ord a div gcd n (ord a)) * q = (n div gcd n (ord a)) * d"
haftmann@65416
   484
      by (simp add: dvd_div_mult)
haftmann@65416
   485
    have cp:"coprime (ord a div gcd n (ord a)) (n div gcd n (ord a))"
haftmann@65416
   486
    proof -
haftmann@65416
   487
      have "coprime (n div gcd n (ord a)) (ord a div gcd n (ord a))"
haftmann@65416
   488
        using div_gcd_coprime[of n "ord a"] ge_1 by fastforce
haftmann@65416
   489
      thus ?thesis by (simp add: gcd.commute)
haftmann@65416
   490
    qed
haftmann@65416
   491
    have dvd_d:"(ord a div gcd n (ord a)) dvd d"
haftmann@65416
   492
    proof -
haftmann@65416
   493
      have "ord a div gcd n (ord a) dvd (n div gcd n (ord a)) * d" using prod_eq
haftmann@65416
   494
        by (metis dvd_triv_right mult.commute)
haftmann@65416
   495
      hence "ord a div gcd n (ord a) dvd d * (n div gcd n (ord a))"
haftmann@65416
   496
        by (simp add:  mult.commute)
haftmann@65416
   497
      thus ?thesis using coprime_dvd_mult[OF cp, of d] by fastforce
haftmann@65416
   498
    qed
haftmann@65416
   499
    have "d > 0" using d_elem by simp
haftmann@65416
   500
    hence "ord a div gcd n (ord a) \<le> d" using dvd_d by (simp add : Nat.dvd_imp_le)
haftmann@65416
   501
    hence False using d_lt by simp
haftmann@65416
   502
  } hence ord_gcd_min: "\<And> d . d \<in> {d \<in> {1..order G}. (a(^)n) (^) d = \<one>}
haftmann@65416
   503
                        \<Longrightarrow> d\<ge>ord a div gcd n (ord a)" by fastforce
haftmann@65416
   504
  have fin:"finite {d \<in> {1..order G}. (a(^)n) (^) d = \<one>}" by auto
haftmann@65416
   505
  thus ?thesis using Min_eqI[OF fin ord_gcd_min ord_gcd_elem]
haftmann@65416
   506
    unfolding ord_def by simp
haftmann@65416
   507
qed
haftmann@65416
   508
haftmann@65416
   509
lemma ord_1_eq_1 :
haftmann@65416
   510
  assumes "finite (carrier G)"
haftmann@65416
   511
  shows "ord \<one> = 1"
haftmann@65416
   512
 using assms ord_ge_1 ord_min[of 1 \<one>] by force
haftmann@65416
   513
haftmann@65416
   514
theorem lagrange_dvd:
haftmann@65416
   515
 assumes "finite(carrier G)" "subgroup H G" shows "(card H) dvd (order G)"
haftmann@65416
   516
 using assms by (simp add: lagrange[symmetric])
haftmann@65416
   517
haftmann@65416
   518
lemma element_generates_subgroup:
haftmann@65416
   519
  assumes finite[simp]: "finite (carrier G)"
haftmann@65416
   520
  assumes a[simp]: "a \<in> carrier G"
haftmann@65416
   521
  shows "subgroup {a (^) i | i. i \<in> {0 .. ord a - 1}} G"
haftmann@65416
   522
proof
haftmann@65416
   523
  show "{a(^)i | i. i \<in> {0 .. ord a - 1} } \<subseteq> carrier G" by auto
haftmann@65416
   524
next
haftmann@65416
   525
  fix x y
haftmann@65416
   526
  assume A: "x \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}" "y \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}"
haftmann@65416
   527
  obtain i::nat where i:"x = a(^)i" and i2:"i \<in> UNIV" using A by auto
haftmann@65416
   528
  obtain j::nat where j:"y = a(^)j" and j2:"j \<in> UNIV" using A by auto
haftmann@65416
   529
  have "a(^)(i+j) \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}" using ord_elems[OF assms] A by auto
haftmann@65416
   530
  thus "x \<otimes> y \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}"
haftmann@65416
   531
    using i j a ord_elems assms by (auto simp add: nat_pow_mult)
haftmann@65416
   532
next
haftmann@65416
   533
  show "\<one> \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}" by force
haftmann@65416
   534
next
haftmann@65416
   535
  fix x assume x: "x \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}"
haftmann@65416
   536
  hence x_in_carrier: "x \<in> carrier G" by auto
haftmann@65416
   537
  then obtain d::nat where d:"x (^) d = \<one>" and "d\<ge>1"
haftmann@65416
   538
    using finite_group_elem_finite_ord by auto
haftmann@65416
   539
  have inv_1:"x(^)(d - 1) \<otimes> x = \<one>" using `d\<ge>1` d nat_pow_Suc[of x "d - 1"] by simp
haftmann@65416
   540
  have elem:"x (^) (d - 1) \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}"
haftmann@65416
   541
  proof -
haftmann@65416
   542
    obtain i::nat where i:"x = a(^)i" using x by auto
haftmann@65416
   543
    hence "x(^)(d - 1) \<in> {a(^)i | i. i \<in> (UNIV::nat set)}" by (auto simp add: nat_pow_pow)
haftmann@65416
   544
    thus ?thesis using ord_elems[of a] by auto
haftmann@65416
   545
  qed
haftmann@65416
   546
  have inv:"inv x = x(^)(d - 1)" using inv_equality[OF inv_1] x_in_carrier by blast
haftmann@65416
   547
  thus "inv x \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}" using elem inv by auto
haftmann@65416
   548
qed
haftmann@65416
   549
haftmann@65416
   550
lemma ord_dvd_group_order :
haftmann@65416
   551
  assumes finite[simp]: "finite (carrier G)"
haftmann@65416
   552
  assumes a[simp]: "a \<in> carrier G"
haftmann@65416
   553
  shows "ord a dvd order G"
haftmann@65416
   554
proof -
haftmann@65416
   555
  have card_dvd:"card {a(^)i | i. i \<in> {0 .. ord a - 1}} dvd card (carrier G)"
haftmann@65416
   556
    using lagrange_dvd element_generates_subgroup unfolding order_def by simp
haftmann@65416
   557
  have "inj_on (\<lambda> i . a(^)i) {0..ord a - 1}" using ord_inj by simp
haftmann@65416
   558
  hence cards_eq:"card ( (\<lambda> i . a(^)i) ` {0..ord a - 1}) = card {0..ord a - 1}"
haftmann@65416
   559
    using card_image[of "\<lambda> i . a(^)i" "{0..ord a - 1}"] by auto
haftmann@65416
   560
  have "(\<lambda> i . a(^)i) ` {0..ord a - 1} = {a(^)i | i. i \<in> {0..ord a - 1}}" by auto
haftmann@65416
   561
  hence "card {a(^)i | i. i \<in> {0..ord a - 1}} = card {0..ord a - 1}" using cards_eq by simp
haftmann@65416
   562
  also have "\<dots> = ord a" using ord_ge_1[of a] by simp
haftmann@65416
   563
  finally show ?thesis using card_dvd by (simp add: order_def)
haftmann@65416
   564
qed
haftmann@65416
   565
haftmann@65416
   566
end
haftmann@65416
   567
haftmann@65416
   568
haftmann@65416
   569
section {* Number of Roots of a Polynomial *}
haftmann@65416
   570
text_raw {* \label{sec:number-roots} *}
haftmann@65416
   571
haftmann@65416
   572
haftmann@65416
   573
definition mult_of :: "('a, 'b) ring_scheme \<Rightarrow> 'a monoid" where
haftmann@65416
   574
  "mult_of R \<equiv> \<lparr> carrier = carrier R - {\<zero>\<^bsub>R\<^esub>}, mult = mult R, one = \<one>\<^bsub>R\<^esub>\<rparr>"
haftmann@65416
   575
haftmann@65416
   576
lemma carrier_mult_of: "carrier (mult_of R) = carrier R - {\<zero>\<^bsub>R\<^esub>}"
haftmann@65416
   577
  by (simp add: mult_of_def)
haftmann@65416
   578
haftmann@65416
   579
lemma mult_mult_of: "mult (mult_of R) = mult R"
haftmann@65416
   580
 by (simp add: mult_of_def)
haftmann@65416
   581
haftmann@65416
   582
lemma nat_pow_mult_of: "op (^)\<^bsub>mult_of R\<^esub> = (op (^)\<^bsub>R\<^esub> :: _ \<Rightarrow> nat \<Rightarrow> _)"
haftmann@65416
   583
  by (simp add: mult_of_def fun_eq_iff nat_pow_def)
haftmann@65416
   584
haftmann@65416
   585
lemma one_mult_of: "\<one>\<^bsub>mult_of R\<^esub> = \<one>\<^bsub>R\<^esub>"
haftmann@65416
   586
  by (simp add: mult_of_def)
haftmann@65416
   587
haftmann@65416
   588
lemmas mult_of_simps = carrier_mult_of mult_mult_of nat_pow_mult_of one_mult_of
haftmann@65416
   589
haftmann@65416
   590
context field begin
haftmann@65416
   591
haftmann@65416
   592
lemma field_mult_group :
haftmann@65416
   593
  shows "group (mult_of R)"
haftmann@65416
   594
  apply (rule groupI)
haftmann@65416
   595
  apply (auto simp: mult_of_simps m_assoc dest: integral)
haftmann@65416
   596
  by (metis Diff_iff Units_inv_Units Units_l_inv field_Units singletonE)
haftmann@65416
   597
haftmann@65416
   598
lemma finite_mult_of: "finite (carrier R) \<Longrightarrow> finite (carrier (mult_of R))"
haftmann@65416
   599
  by (auto simp: mult_of_simps)
haftmann@65416
   600
haftmann@65416
   601
lemma order_mult_of: "finite (carrier R) \<Longrightarrow> order (mult_of R) = order R - 1"
haftmann@65416
   602
  unfolding order_def carrier_mult_of by (simp add: card.remove)
haftmann@65416
   603
haftmann@65416
   604
end
haftmann@65416
   605
haftmann@65416
   606
haftmann@65416
   607
haftmann@65416
   608
lemma (in monoid) Units_pow_closed :
haftmann@65416
   609
  fixes d :: nat
haftmann@65416
   610
  assumes "x \<in> Units G"
haftmann@65416
   611
  shows "x (^) d \<in> Units G"
haftmann@65416
   612
    by (metis assms group.is_monoid monoid.nat_pow_closed units_group units_of_carrier units_of_pow)
haftmann@65416
   613
haftmann@65416
   614
lemma (in comm_monoid) is_monoid:
haftmann@65416
   615
  shows "monoid G" by unfold_locales
haftmann@65416
   616
haftmann@65416
   617
declare comm_monoid.is_monoid[intro?]
haftmann@65416
   618
haftmann@65416
   619
lemma (in ring) r_right_minus_eq[simp]:
haftmann@65416
   620
  assumes "a \<in> carrier R" "b \<in> carrier R"
haftmann@65416
   621
  shows "a \<ominus> b = \<zero> \<longleftrightarrow> a = b"
haftmann@65416
   622
  using assms by (metis a_minus_def add.inv_closed minus_equality r_neg)
haftmann@65416
   623
haftmann@65416
   624
context UP_cring begin
haftmann@65416
   625
haftmann@65416
   626
lemma is_UP_cring:"UP_cring R" by (unfold_locales)
haftmann@65416
   627
lemma is_UP_ring :
haftmann@65416
   628
  shows "UP_ring R" by (unfold_locales)
haftmann@65416
   629
haftmann@65416
   630
end
haftmann@65416
   631
haftmann@65416
   632
context UP_domain begin
haftmann@65416
   633
haftmann@65416
   634
haftmann@65416
   635
lemma roots_bound:
haftmann@65416
   636
  assumes f [simp]: "f \<in> carrier P"
haftmann@65416
   637
  assumes f_not_zero: "f \<noteq> \<zero>\<^bsub>P\<^esub>"
haftmann@65416
   638
  assumes finite: "finite (carrier R)"
haftmann@65416
   639
  shows "finite {a \<in> carrier R . eval R R id a f = \<zero>} \<and>
haftmann@65416
   640
         card {a \<in> carrier R . eval R R id a f = \<zero>} \<le> deg R f" using f f_not_zero
haftmann@65416
   641
proof (induction "deg R f" arbitrary: f)
haftmann@65416
   642
  case 0
haftmann@65416
   643
  have "\<And>x. eval R R id x f \<noteq> \<zero>"
haftmann@65416
   644
  proof -
haftmann@65416
   645
    fix x
haftmann@65416
   646
    have "(\<Oplus>i\<in>{..deg R f}. id (coeff P f i) \<otimes> x (^) i) \<noteq> \<zero>"
haftmann@65416
   647
      using 0 lcoeff_nonzero_nonzero[where p = f] by simp
haftmann@65416
   648
    thus "eval R R id x f \<noteq> \<zero>" using 0 unfolding eval_def P_def by simp
haftmann@65416
   649
  qed
haftmann@65416
   650
  then have *: "{a \<in> carrier R. eval R R (\<lambda>a. a) a f = \<zero>} = {}"
haftmann@65416
   651
    by (auto simp: id_def)
haftmann@65416
   652
  show ?case by (simp add: *)
haftmann@65416
   653
next
haftmann@65416
   654
  case (Suc x)
haftmann@65416
   655
  show ?case
haftmann@65416
   656
  proof (cases "\<exists> a \<in> carrier R . eval R R id a f = \<zero>")
haftmann@65416
   657
    case True
haftmann@65416
   658
    then obtain a where a_carrier[simp]: "a \<in> carrier R" and a_root:"eval R R id a f = \<zero>" by blast
haftmann@65416
   659
    have R_not_triv: "carrier R \<noteq> {\<zero>}"
haftmann@65416
   660
      by (metis R.one_zeroI R.zero_not_one)
haftmann@65416
   661
    obtain q  where q:"(q \<in> carrier P)" and
haftmann@65416
   662
      f:"f = (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub> P\<^esub> monom P a 0) \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> monom P (eval R R id a f) 0"
haftmann@65416
   663
     using remainder_theorem[OF Suc.prems(1) a_carrier R_not_triv] by auto
haftmann@65416
   664
    hence lin_fac: "f = (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub> P\<^esub> monom P a 0) \<otimes>\<^bsub>P\<^esub> q" using q by (simp add: a_root)
haftmann@65416
   665
    have deg:"deg R (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub> P\<^esub> monom P a 0) = 1"
haftmann@65416
   666
      using a_carrier by (simp add: deg_minus_eq)
haftmann@65416
   667
    hence mon_not_zero:"(monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub> P\<^esub> monom P a 0) \<noteq> \<zero>\<^bsub>P\<^esub>"
haftmann@65416
   668
      by (fastforce simp del: r_right_minus_eq)
haftmann@65416
   669
    have q_not_zero:"q \<noteq> \<zero>\<^bsub>P\<^esub>" using Suc by (auto simp add : lin_fac)
haftmann@65416
   670
    hence "deg R q = x" using Suc deg deg_mult[OF mon_not_zero q_not_zero _ q]
haftmann@65416
   671
      by (simp add : lin_fac)
haftmann@65416
   672
    hence q_IH:"finite {a \<in> carrier R . eval R R id a q = \<zero>}
haftmann@65416
   673
                \<and> card {a \<in> carrier R . eval R R id a q = \<zero>} \<le> x" using Suc q q_not_zero by blast
haftmann@65416
   674
    have subs:"{a \<in> carrier R . eval R R id a f = \<zero>}
haftmann@65416
   675
                \<subseteq> {a \<in> carrier R . eval R R id a q = \<zero>} \<union> {a}" (is "?L \<subseteq> ?R \<union> {a}")
haftmann@65416
   676
      using a_carrier `q \<in> _`
haftmann@65416
   677
      by (auto simp: evalRR_simps lin_fac R.integral_iff)
haftmann@65416
   678
    have "{a \<in> carrier R . eval R R id a f = \<zero>} \<subseteq> insert a {a \<in> carrier R . eval R R id a q = \<zero>}"
haftmann@65416
   679
     using subs by auto
haftmann@65416
   680
    hence "card {a \<in> carrier R . eval R R id a f = \<zero>} \<le>
haftmann@65416
   681
           card (insert a {a \<in> carrier R . eval R R id a q = \<zero>})" using q_IH by (blast intro: card_mono)
haftmann@65416
   682
    also have "\<dots> \<le> deg R f" using q_IH `Suc x = _`
haftmann@65416
   683
      by (simp add: card_insert_if)
haftmann@65416
   684
    finally show ?thesis using q_IH `Suc x = _` using finite by force
haftmann@65416
   685
  next
haftmann@65416
   686
    case False
haftmann@65416
   687
    hence "card {a \<in> carrier R. eval R R id a f = \<zero>} = 0" using finite by auto
haftmann@65416
   688
    also have "\<dots> \<le>  deg R f" by simp
haftmann@65416
   689
    finally show ?thesis using finite by auto
haftmann@65416
   690
  qed
haftmann@65416
   691
qed
haftmann@65416
   692
haftmann@65416
   693
end
haftmann@65416
   694
haftmann@65416
   695
lemma (in domain) num_roots_le_deg :
haftmann@65416
   696
  fixes p d :: nat
haftmann@65416
   697
  assumes finite:"finite (carrier R)"
haftmann@65416
   698
  assumes d_neq_zero : "d \<noteq> 0"
haftmann@65416
   699
  shows "card {x \<in> carrier R. x (^) d = \<one>} \<le> d"
haftmann@65416
   700
proof -
haftmann@65416
   701
  let ?f = "monom (UP R) \<one>\<^bsub>R\<^esub> d \<ominus>\<^bsub> (UP R)\<^esub> monom (UP R) \<one>\<^bsub>R\<^esub> 0"
haftmann@65416
   702
  have one_in_carrier:"\<one> \<in> carrier R" by simp
haftmann@65416
   703
  interpret R: UP_domain R "UP R" by (unfold_locales)
haftmann@65416
   704
  have "deg R ?f = d"
haftmann@65416
   705
    using d_neq_zero by (simp add: R.deg_minus_eq)
haftmann@65416
   706
  hence f_not_zero:"?f \<noteq> \<zero>\<^bsub>UP R\<^esub>" using  d_neq_zero by (auto simp add : R.deg_nzero_nzero)
haftmann@65416
   707
  have roots_bound:"finite {a \<in> carrier R . eval R R id a ?f = \<zero>} \<and>
haftmann@65416
   708
                    card {a \<in> carrier R . eval R R id a ?f = \<zero>} \<le> deg R ?f"
haftmann@65416
   709
                    using finite by (intro R.roots_bound[OF _ f_not_zero]) simp
haftmann@65416
   710
  have subs:"{x \<in> carrier R. x (^) d = \<one>} \<subseteq> {a \<in> carrier R . eval R R id a ?f = \<zero>}"
haftmann@65416
   711
    by (auto simp: R.evalRR_simps)
haftmann@65416
   712
  then have "card {x \<in> carrier R. x (^) d = \<one>} \<le>
haftmann@65416
   713
        card {a \<in> carrier R. eval R R id a ?f = \<zero>}" using finite by (simp add : card_mono)
haftmann@65416
   714
  thus ?thesis using `deg R ?f = d` roots_bound by linarith
haftmann@65416
   715
qed
haftmann@65416
   716
haftmann@65416
   717
haftmann@65416
   718
haftmann@65416
   719
section {* The Multiplicative Group of a Field *}
haftmann@65416
   720
text_raw {* \label{sec:mult-group} *}
haftmann@65416
   721
haftmann@65416
   722
haftmann@65416
   723
text {*
haftmann@65416
   724
  In this section we show that the multiplicative group of a finite field
haftmann@65416
   725
  is generated by a single element, i.e. it is cyclic. The proof is inspired
haftmann@65416
   726
  by the first proof given in the survey~\cite{conrad-cyclicity}.
haftmann@65416
   727
*}
haftmann@65416
   728
haftmann@65416
   729
lemma (in group) pow_order_eq_1:
haftmann@65416
   730
  assumes "finite (carrier G)" "x \<in> carrier G" shows "x (^) order G = \<one>"
haftmann@65416
   731
  using assms by (metis nat_pow_pow ord_dvd_group_order pow_ord_eq_1 dvdE nat_pow_one)
haftmann@65416
   732
haftmann@65416
   733
(* XXX remove in AFP devel, replaced by div_eq_dividend_iff *)
haftmann@65416
   734
lemma nat_div_eq: "a \<noteq> 0 \<Longrightarrow> (a :: nat) div b = a \<longleftrightarrow> b = 1"
haftmann@65416
   735
  apply rule
haftmann@65416
   736
  apply (cases "b = 0")
haftmann@65416
   737
  apply simp_all
haftmann@65416
   738
  apply (metis (full_types) One_nat_def Suc_lessI div_less_dividend less_not_refl3)
haftmann@65416
   739
  done
haftmann@65416
   740
haftmann@65416
   741
lemma (in group)
haftmann@65416
   742
  assumes finite': "finite (carrier G)"
haftmann@65416
   743
  assumes "a \<in> carrier G"
haftmann@65416
   744
  shows pow_ord_eq_ord_iff: "group.ord G (a (^) k) = ord a \<longleftrightarrow> coprime k (ord a)" (is "?L \<longleftrightarrow> ?R")
haftmann@65416
   745
proof
haftmann@65416
   746
  assume A: ?L then show ?R
haftmann@65416
   747
    using assms ord_ge_1[OF assms] by (auto simp: nat_div_eq ord_pow_dvd_ord_elem)
haftmann@65416
   748
next
haftmann@65416
   749
  assume ?R then show ?L
haftmann@65416
   750
    using ord_pow_dvd_ord_elem[OF assms, of k] by auto
haftmann@65416
   751
qed
haftmann@65416
   752
haftmann@65416
   753
context field begin
haftmann@65416
   754
haftmann@65416
   755
lemma num_elems_of_ord_eq_phi':
haftmann@65416
   756
  assumes finite: "finite (carrier R)" and dvd: "d dvd order (mult_of R)"
haftmann@65416
   757
      and exists: "\<exists>a\<in>carrier (mult_of R). group.ord (mult_of R) a = d"
haftmann@65416
   758
  shows "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} = phi' d"
haftmann@65416
   759
proof -
haftmann@65416
   760
  note mult_of_simps[simp]
haftmann@65416
   761
  have finite': "finite (carrier (mult_of R))" using finite by (rule finite_mult_of)
haftmann@65416
   762
haftmann@65416
   763
  interpret G:group "mult_of R" rewrites "op (^)\<^bsub>mult_of R\<^esub> = (op (^) :: _ \<Rightarrow> nat \<Rightarrow> _)" and "\<one>\<^bsub>mult_of R\<^esub> = \<one>"
haftmann@65416
   764
    by (rule field_mult_group) simp_all
haftmann@65416
   765
haftmann@65416
   766
  from exists
haftmann@65416
   767
  obtain a where a:"a \<in> carrier (mult_of R)" and ord_a: "group.ord (mult_of R) a = d"
haftmann@65416
   768
    by (auto simp add: card_gt_0_iff)
haftmann@65416
   769
haftmann@65416
   770
  have set_eq1:"{a(^)n| n. n \<in> {1 .. d}} = {x \<in> carrier (mult_of R). x (^) d = \<one>}"
haftmann@65416
   771
  proof (rule card_seteq)
haftmann@65416
   772
    show "finite {x \<in> carrier (mult_of R). x (^) d = \<one>}" using finite by auto
haftmann@65416
   773
haftmann@65416
   774
    show "{a(^)n| n. n \<in> {1 ..d}} \<subseteq> {x \<in> carrier (mult_of R). x(^)d = \<one>}"
haftmann@65416
   775
    proof
haftmann@65416
   776
      fix x assume "x \<in> {a(^)n | n. n \<in> {1 .. d}}"
haftmann@65416
   777
      then obtain n where n:"x = a(^)n \<and> n \<in> {1 .. d}" by auto
haftmann@65416
   778
      have "x(^)d =(a(^)d)(^)n" using n a ord_a by (simp add:nat_pow_pow mult.commute)
haftmann@65416
   779
      hence "x(^)d = \<one>" using ord_a G.pow_ord_eq_1[OF finite' a] by fastforce
haftmann@65416
   780
      thus "x \<in> {x \<in> carrier (mult_of R). x(^)d = \<one>}" using G.nat_pow_closed[OF a] n by blast
haftmann@65416
   781
    qed
haftmann@65416
   782
haftmann@65416
   783
    show "card {x \<in> carrier (mult_of R). x (^) d = \<one>} \<le> card {a(^)n | n. n \<in> {1 .. d}}"
haftmann@65416
   784
    proof -
haftmann@65416
   785
      have *:"{a(^)n | n. n \<in> {1 .. d }} = ((\<lambda> n. a(^)n) ` {1 .. d})" by auto
haftmann@65416
   786
      have "0 < order (mult_of R)" unfolding order_mult_of[OF finite]
haftmann@65416
   787
        using card_mono[OF finite, of "{\<zero>, \<one>}"] by (simp add: order_def)
haftmann@65416
   788
      have "card {x \<in> carrier (mult_of R). x (^) d = \<one>} \<le> card {x \<in> carrier R. x (^) d = \<one>}"
haftmann@65416
   789
        using finite by (auto intro: card_mono)
haftmann@65416
   790
      also have "\<dots> \<le> d" using `0 < order (mult_of R)` num_roots_le_deg[OF finite, of d]
haftmann@65416
   791
        by (simp add : dvd_pos_nat[OF _ `d dvd order (mult_of R)`])
haftmann@65416
   792
      finally show ?thesis using G.ord_inj'[OF finite' a] ord_a * by (simp add: card_image)
haftmann@65416
   793
    qed
haftmann@65416
   794
  qed
haftmann@65416
   795
haftmann@65416
   796
  have set_eq2:"{x \<in> carrier (mult_of R) . group.ord (mult_of R) x = d}
haftmann@65416
   797
                = (\<lambda> n . a(^)n) ` {n \<in> {1 .. d}. group.ord (mult_of R) (a(^)n) = d}" (is "?L = ?R")
haftmann@65416
   798
  proof
haftmann@65416
   799
    { fix x assume x:"x \<in> (carrier (mult_of R)) \<and> group.ord (mult_of R) x = d"
haftmann@65416
   800
      hence "x \<in> {x \<in> carrier (mult_of R). x (^) d = \<one>}"
haftmann@65416
   801
        by (simp add: G.pow_ord_eq_1[OF finite', of x, symmetric])
haftmann@65416
   802
      then obtain n where n:"x = a(^)n \<and> n \<in> {1 .. d}" using set_eq1 by blast
haftmann@65416
   803
      hence "x \<in> ?R" using x by fast
haftmann@65416
   804
    } thus "?L \<subseteq> ?R" by blast
haftmann@65416
   805
    show "?R \<subseteq> ?L" using a by (auto simp add: carrier_mult_of[symmetric] simp del: carrier_mult_of)
haftmann@65416
   806
  qed
haftmann@65416
   807
  have "inj_on (\<lambda> n . a(^)n) {n \<in> {1 .. d}. group.ord (mult_of R) (a(^)n) = d}"
haftmann@65416
   808
    using G.ord_inj'[OF finite' a, unfolded ord_a] unfolding inj_on_def by fast
haftmann@65416
   809
  hence "card ((\<lambda>n. a(^)n) ` {n \<in> {1 .. d}. group.ord (mult_of R) (a(^)n) = d})
haftmann@65416
   810
         = card {k \<in> {1 .. d}. group.ord (mult_of R) (a(^)k) = d}"
haftmann@65416
   811
         using card_image by blast
haftmann@65416
   812
  thus ?thesis using set_eq2 G.pow_ord_eq_ord_iff[OF finite' `a \<in> _`, unfolded ord_a]
haftmann@65416
   813
    by (simp add: phi'_def)
haftmann@65416
   814
qed
haftmann@65416
   815
haftmann@65416
   816
end
haftmann@65416
   817
haftmann@65416
   818
haftmann@65416
   819
theorem (in field) finite_field_mult_group_has_gen :
haftmann@65416
   820
  assumes finite:"finite (carrier R)"
haftmann@65416
   821
  shows "\<exists> a \<in> carrier (mult_of R) . carrier (mult_of R) = {a(^)i | i::nat . i \<in> UNIV}"
haftmann@65416
   822
proof -
haftmann@65416
   823
  note mult_of_simps[simp]
haftmann@65416
   824
  have finite': "finite (carrier (mult_of R))" using finite by (rule finite_mult_of)
haftmann@65416
   825
haftmann@65416
   826
  interpret G: group "mult_of R" rewrites
haftmann@65416
   827
      "op (^)\<^bsub>mult_of R\<^esub> = (op (^) :: _ \<Rightarrow> nat \<Rightarrow> _)" and "\<one>\<^bsub>mult_of R\<^esub> = \<one>"
haftmann@65416
   828
    by (rule field_mult_group) (simp_all add: fun_eq_iff nat_pow_def)
haftmann@65416
   829
haftmann@65416
   830
  let ?N = "\<lambda> x . card {a \<in> carrier (mult_of R). group.ord (mult_of R) a  = x}"
haftmann@65416
   831
  have "0 < order R - 1" unfolding order_def using card_mono[OF finite, of "{\<zero>, \<one>}"] by simp
haftmann@65416
   832
  then have *: "0 < order (mult_of R)" using assms by (simp add: order_mult_of)
haftmann@65416
   833
  have fin: "finite {d. d dvd order (mult_of R) }" using dvd_nat_bounds[OF *] by force
haftmann@65416
   834
haftmann@65416
   835
  have "(\<Sum>d | d dvd order (mult_of R). ?N d)
haftmann@65416
   836
      = card (UN d:{d . d dvd order (mult_of R) }. {a \<in> carrier (mult_of R). group.ord (mult_of R) a  = d})"
haftmann@65416
   837
      (is "_ = card ?U")
haftmann@65416
   838
    using fin finite by (subst card_UN_disjoint) auto
haftmann@65416
   839
  also have "?U = carrier (mult_of R)"
haftmann@65416
   840
  proof
haftmann@65416
   841
    { fix x assume x:"x \<in> carrier (mult_of R)"
haftmann@65416
   842
      hence x':"x\<in>carrier (mult_of R)" by simp
haftmann@65416
   843
      then have "group.ord (mult_of R) x dvd order (mult_of R)"
haftmann@65416
   844
          using finite' G.ord_dvd_group_order[OF _ x'] by (simp add: order_mult_of)
haftmann@65416
   845
      hence "x \<in> ?U" using dvd_nat_bounds[of "order (mult_of R)" "group.ord (mult_of R) x"] x by blast
haftmann@65416
   846
    } thus "carrier (mult_of R) \<subseteq> ?U" by blast
haftmann@65416
   847
  qed auto
haftmann@65416
   848
  also have "card ... = order (mult_of R)"
haftmann@65416
   849
    using order_mult_of finite' by (simp add: order_def)
haftmann@65416
   850
  finally have sum_Ns_eq: "(\<Sum>d | d dvd order (mult_of R). ?N d) = order (mult_of R)" .
haftmann@65416
   851
haftmann@65416
   852
  { fix d assume d:"d dvd order (mult_of R)"
haftmann@65416
   853
    have "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} \<le> phi' d"
haftmann@65416
   854
    proof cases
haftmann@65416
   855
      assume "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} = 0" thus ?thesis by presburger
haftmann@65416
   856
      next
haftmann@65416
   857
      assume "card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = d} \<noteq> 0"
haftmann@65416
   858
      hence "\<exists>a \<in> carrier (mult_of R). group.ord (mult_of R) a = d" by (auto simp: card_eq_0_iff)
haftmann@65416
   859
      thus ?thesis using num_elems_of_ord_eq_phi'[OF finite d] by auto
haftmann@65416
   860
    qed
haftmann@65416
   861
  }
haftmann@65416
   862
  hence all_le:"\<And>i. i \<in> {d. d dvd order (mult_of R) }
haftmann@65416
   863
        \<Longrightarrow> (\<lambda>i. card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = i}) i \<le> (\<lambda>i. phi' i) i" by fast
haftmann@65416
   864
  hence le:"(\<Sum>i | i dvd order (mult_of R). ?N i)
haftmann@65416
   865
            \<le> (\<Sum>i | i dvd order (mult_of R). phi' i)"
haftmann@65416
   866
            using sum_mono[of "{d .  d dvd order (mult_of R)}"
haftmann@65416
   867
                  "\<lambda>i. card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = i}"] by presburger
haftmann@65416
   868
  have "order (mult_of R) = (\<Sum>d | d dvd order (mult_of R). phi' d)" using *
haftmann@65416
   869
    by (simp add: sum_phi'_factors)
haftmann@65416
   870
  hence eq:"(\<Sum>i | i dvd order (mult_of R). ?N i)
haftmann@65416
   871
          = (\<Sum>i | i dvd order (mult_of R). phi' i)" using le sum_Ns_eq by presburger
haftmann@65416
   872
  have "\<And>i. i \<in> {d. d dvd order (mult_of R) } \<Longrightarrow> ?N i = (\<lambda>i. phi' i) i"
haftmann@65416
   873
  proof (rule ccontr)
haftmann@65416
   874
    fix i
haftmann@65416
   875
    assume i1:"i \<in> {d. d dvd order (mult_of R)}" and "?N i \<noteq> phi' i"
haftmann@65416
   876
    hence "?N i = 0"
haftmann@65416
   877
      using num_elems_of_ord_eq_phi'[OF finite, of i] by (auto simp: card_eq_0_iff)
haftmann@65416
   878
    moreover  have "0 < i" using * i1 by (simp add: dvd_nat_bounds[of "order (mult_of R)" i])
haftmann@65416
   879
    ultimately have "?N i < phi' i" using phi'_nonzero by presburger
haftmann@65416
   880
    hence "(\<Sum>i | i dvd order (mult_of R). ?N i)
haftmann@65416
   881
         < (\<Sum>i | i dvd order (mult_of R). phi' i)"
haftmann@65416
   882
      using sum_strict_mono_ex1[OF fin, of "?N" "\<lambda> i . phi' i"]
haftmann@65416
   883
            i1 all_le by auto
haftmann@65416
   884
    thus False using eq by force
haftmann@65416
   885
  qed
haftmann@65416
   886
  hence "?N (order (mult_of R)) > 0" using * by (simp add: phi'_nonzero)
haftmann@65416
   887
  then obtain a where a:"a \<in> carrier (mult_of R)" and a_ord:"group.ord (mult_of R) a = order (mult_of R)"
haftmann@65416
   888
    by (auto simp add: card_gt_0_iff)
haftmann@65416
   889
  hence set_eq:"{a(^)i | i::nat. i \<in> UNIV} = (\<lambda>x. a(^)x) ` {0 .. group.ord (mult_of R) a - 1}"
haftmann@65416
   890
    using G.ord_elems[OF finite'] by auto
haftmann@65416
   891
  have card_eq:"card ((\<lambda>x. a(^)x) ` {0 .. group.ord (mult_of R) a - 1}) = card {0 .. group.ord (mult_of R) a - 1}"
haftmann@65416
   892
    by (intro card_image G.ord_inj finite' a)
haftmann@65416
   893
  hence "card ((\<lambda> x . a(^)x) ` {0 .. group.ord (mult_of R) a - 1}) = card {0 ..order (mult_of R) - 1}"
haftmann@65416
   894
    using assms by (simp add: card_eq a_ord)
haftmann@65416
   895
  hence card_R_minus_1:"card {a(^)i | i::nat. i \<in> UNIV} =  order (mult_of R)"
haftmann@65416
   896
    using * by (subst set_eq) auto
haftmann@65416
   897
  have **:"{a(^)i | i::nat. i \<in> UNIV} \<subseteq> carrier (mult_of R)"
haftmann@65416
   898
    using G.nat_pow_closed[OF a] by auto
haftmann@65416
   899
  with _ have "carrier (mult_of R) = {a(^)i|i::nat. i \<in> UNIV}"
haftmann@65416
   900
    by (rule card_seteq[symmetric]) (simp_all add: card_R_minus_1 finite order_def del: UNIV_I)
haftmann@65416
   901
  thus ?thesis using a by blast
haftmann@65416
   902
qed
haftmann@65416
   903
haftmann@65416
   904
end