src/HOL/Number_Theory/Residues.thy
changeset 66304 cde6ceffcbc7
parent 65899 ab7d8c999531
child 66305 7454317f883c
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Tue Aug 01 17:30:02 2017 +0200
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Tue Aug 01 17:33:04 2017 +0200
     1.3 @@ -378,9 +378,9 @@
     1.4      by (metis residues_prime.wilson_theorem1 residues_prime.intro le_eq_less_or_eq)
     1.5  qed
     1.6  
     1.7 -text {*
     1.8 +text \<open>
     1.9    This result can be transferred to the multiplicative group of
    1.10 -  $\mathbb{Z}/p\mathbb{Z}$ for $p$ prime. *}
    1.11 +  $\mathbb{Z}/p\mathbb{Z}$ for $p$ prime.\<close>
    1.12  
    1.13  lemma mod_nat_int_pow_eq:
    1.14    fixes n :: nat and p a :: int
    1.15 @@ -409,22 +409,22 @@
    1.16    have **:"nat ` {1 .. int p - 1} = {1 .. p - 1}" (is "?L = ?R")
    1.17    proof
    1.18      { fix n assume n: "n \<in> ?L"
    1.19 -      then have "n \<in> ?R" using `p\<ge>2` by force
    1.20 +      then have "n \<in> ?R" using \<open>p\<ge>2\<close> by force
    1.21      } thus "?L \<subseteq> ?R" by blast
    1.22      { fix n assume n: "n \<in> ?R"
    1.23 -      then have "n \<in> ?L" using `p\<ge>2` Set_Interval.transfer_nat_int_set_functions(2) by fastforce
    1.24 +      then have "n \<in> ?L" using \<open>p\<ge>2\<close> Set_Interval.transfer_nat_int_set_functions(2) by fastforce
    1.25      } thus "?R \<subseteq> ?L" by blast
    1.26    qed
    1.27    have "nat ` {a^i mod (int p) | i::nat. i \<in> UNIV} = {nat a^i mod p | i . i \<in> UNIV}" (is "?L = ?R")
    1.28    proof
    1.29      { fix x assume x: "x \<in> ?L"
    1.30        then obtain i where i:"x = nat (a^i mod (int p))" by blast
    1.31 -      hence "x = nat a ^ i mod p" using mod_nat_int_pow_eq[of a "int p" i] a `p\<ge>2` by auto
    1.32 +      hence "x = nat a ^ i mod p" using mod_nat_int_pow_eq[of a "int p" i] a \<open>p\<ge>2\<close> by auto
    1.33        hence "x \<in> ?R" using i by blast
    1.34      } thus "?L \<subseteq> ?R" by blast
    1.35      { fix x assume x: "x \<in> ?R"
    1.36        then obtain i where i:"x = nat a^i mod p" by blast
    1.37 -      hence "x \<in> ?L" using mod_nat_int_pow_eq[of a "int p" i] a `p\<ge>2` by auto
    1.38 +      hence "x \<in> ?L" using mod_nat_int_pow_eq[of a "int p" i] a \<open>p\<ge>2\<close> by auto
    1.39      } thus "?R \<subseteq> ?L" by blast
    1.40    qed
    1.41    hence "{1 .. p - 1} = {nat a^i mod p | i. i \<in> UNIV}"