equal
deleted
inserted
replaced
8 section \<open>Residue rings\<close> |
8 section \<open>Residue rings\<close> |
9 |
9 |
10 theory Residues |
10 theory Residues |
11 imports |
11 imports |
12 Cong |
12 Cong |
13 "~~/src/HOL/Algebra/More_Group" |
13 "HOL-Algebra.More_Group" |
14 "~~/src/HOL/Algebra/More_Ring" |
14 "HOL-Algebra.More_Ring" |
15 "~~/src/HOL/Algebra/More_Finite_Product" |
15 "HOL-Algebra.More_Finite_Product" |
16 "~~/src/HOL/Algebra/Multiplicative_Group" |
16 "HOL-Algebra.Multiplicative_Group" |
17 Totient |
17 Totient |
18 begin |
18 begin |
19 |
19 |
20 definition QuadRes :: "int \<Rightarrow> int \<Rightarrow> bool" |
20 definition QuadRes :: "int \<Rightarrow> int \<Rightarrow> bool" |
21 where "QuadRes p a = (\<exists>y. ([y^2 = a] (mod p)))" |
21 where "QuadRes p a = (\<exists>y. ([y^2 = a] (mod p)))" |