src/HOL/Number_Theory/Residues.thy
 changeset 69785 9e326f6f8a24 parent 68458 023b353911c5
```     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Sat Feb 02 15:52:14 2019 +0100
1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Mon Feb 04 12:16:03 2019 +0100
1.3 @@ -398,7 +398,7 @@
1.4    shows "a \<ge> 0 \<Longrightarrow> p \<ge> 0 \<Longrightarrow> (nat a ^ n) mod (nat p) = nat ((a ^ n) mod p)"
1.5    by (simp add: int_one_le_iff_zero_less nat_mod_distrib order_less_imp_le nat_power_eq[symmetric])
1.6
1.7 -theorem residue_prime_mult_group_has_gen :
1.8 +theorem residue_prime_mult_group_has_gen:
1.9   fixes p :: nat
1.10   assumes prime_p : "prime p"
1.11   shows "\<exists>a \<in> {1 .. p - 1}. {1 .. p - 1} = {a^i mod p|i . i \<in> UNIV}"
1.12 @@ -455,4 +455,52 @@
1.13    ultimately show ?thesis ..
1.14  qed
1.15
1.16 +
1.17 +subsection \<open>Upper bound for the number of \$n\$-th roots\<close>
1.18 +
1.19 +lemma roots_mod_prime_bound:
1.20 +  fixes n c p :: nat
1.21 +  assumes "prime p" "n > 0"
1.22 +  defines "A \<equiv> {x\<in>{..<p}. [x ^ n = c] (mod p)}"
1.23 +  shows   "card A \<le> n"
1.24 +proof -
1.25 +  define R where "R = residue_ring (int p)"
1.26 +  term monom
1.27 +  from assms(1) interpret residues_prime p R
1.28 +    by unfold_locales (simp_all add: R_def)
1.29 +  interpret R: UP_domain R "UP R" by (unfold_locales)
1.30 +
1.31 +  let ?f = "UnivPoly.monom (UP R) \<one>\<^bsub>R\<^esub> n \<ominus>\<^bsub>(UP R)\<^esub> UnivPoly.monom (UP R) (int (c mod p)) 0"
1.32 +  have in_carrier: "int (c mod p) \<in> carrier R"
1.33 +    using prime_gt_1_nat[OF assms(1)] by (simp add: R_def residue_ring_def)
1.34 +
1.35 +  have "deg R ?f = n"
1.36 +    using assms in_carrier by (simp add: R.deg_minus_eq)
1.37 +  hence f_not_zero: "?f \<noteq> \<zero>\<^bsub>UP R\<^esub>" using assms by (auto simp add : R.deg_nzero_nzero)
1.38 +  have roots_bound: "finite {a \<in> carrier R. UnivPoly.eval R R id a ?f = \<zero>\<^bsub>R\<^esub>} \<and>
1.39 +                     card {a \<in> carrier R. UnivPoly.eval R R id a ?f = \<zero>\<^bsub>R\<^esub>} \<le> deg R ?f"
1.40 +                    using finite in_carrier by (intro R.roots_bound[OF _ f_not_zero]) simp
1.41 +  have subs: "{x \<in> carrier R. x [^]\<^bsub>R\<^esub> n = int (c mod p)} \<subseteq>
1.42 +                {a \<in> carrier R. UnivPoly.eval R R id a ?f = \<zero>\<^bsub>R\<^esub>}"
1.43 +    using in_carrier by (auto simp: R.evalRR_simps)
1.44 +  then have "card {x \<in> carrier R. x [^]\<^bsub>R\<^esub> n = int (c mod p)} \<le>
1.45 +               card {a \<in> carrier R. UnivPoly.eval R R id a ?f = \<zero>\<^bsub>R\<^esub>}"
1.46 +    using finite by (intro card_mono) auto
1.47 +  also have "\<dots> \<le> n"
1.48 +    using \<open>deg R ?f = n\<close> roots_bound by linarith
1.49 +  also {
1.50 +    fix x assume "x \<in> carrier R"
1.51 +    hence "x [^]\<^bsub>R\<^esub> n = (x ^ n) mod (int p)"
1.52 +      by (subst pow_cong [symmetric]) (auto simp: R_def residue_ring_def)
1.53 +  }
1.54 +  hence "{x \<in> carrier R. x [^]\<^bsub>R\<^esub> n = int (c mod p)} = {x \<in> carrier R. [x ^ n = int c] (mod p)}"
1.55 +    by (fastforce simp: cong_def zmod_int)
1.56 +  also have "bij_betw int A {x \<in> carrier R. [x ^ n = int c] (mod p)}"
1.57 +    by (rule bij_betwI[of int _ _ nat])
1.58 +       (use cong_int_iff in \<open>force simp: R_def residue_ring_def A_def\<close>)+
1.59 +  from bij_betw_same_card[OF this] have "card {x \<in> carrier R. [x ^ n = int c] (mod p)} = card A" ..
1.60 +  finally show ?thesis .
1.61 +qed
1.62 +
1.63 +
1.64  end
```