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 Cong MiscAlgebra |
11 imports Cong MiscAlgebra |
12 begin |
12 begin |
|
13 |
|
14 definition QuadRes :: "int \<Rightarrow> int \<Rightarrow> bool" where |
|
15 "QuadRes p a = (\<exists>y. ([y^2 = a] (mod p)))" |
|
16 |
|
17 definition Legendre :: "int \<Rightarrow> int \<Rightarrow> int" where |
|
18 "Legendre a p = (if ([a = 0] (mod p)) then 0 |
|
19 else if QuadRes p a then 1 |
|
20 else -1)" |
13 |
21 |
14 subsection \<open>A locale for residue rings\<close> |
22 subsection \<open>A locale for residue rings\<close> |
15 |
23 |
16 definition residue_ring :: "int \<Rightarrow> int ring" |
24 definition residue_ring :: "int \<Rightarrow> int ring" |
17 where |
25 where |