src/HOL/Number_Theory/Residues.thy
changeset 64282 261d42f0bfac
parent 64272 f76b6dda2e56
child 64593 50c715579715
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Tue Oct 18 07:04:08 2016 +0200
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Mon Oct 17 15:20:06 2016 +0200
     1.3 @@ -11,6 +11,14 @@
     1.4  imports Cong MiscAlgebra
     1.5  begin
     1.6  
     1.7 +definition QuadRes :: "int \<Rightarrow> int \<Rightarrow> bool" where
     1.8 +  "QuadRes p a = (\<exists>y. ([y^2 = a] (mod p)))"
     1.9 +
    1.10 +definition Legendre :: "int \<Rightarrow> int \<Rightarrow> int" where
    1.11 +  "Legendre a p = (if ([a = 0] (mod p)) then 0
    1.12 +    else if QuadRes p a then 1
    1.13 +    else -1)"
    1.14 +
    1.15  subsection \<open>A locale for residue rings\<close>
    1.16  
    1.17  definition residue_ring :: "int \<Rightarrow> int ring"