--- a/src/HOL/Number_Theory/Residues.thy Tue Oct 18 07:04:08 2016 +0200
+++ b/src/HOL/Number_Theory/Residues.thy Mon Oct 17 15:20:06 2016 +0200
@@ -11,6 +11,14 @@
imports Cong MiscAlgebra
begin
+definition QuadRes :: "int \<Rightarrow> int \<Rightarrow> bool" where
+ "QuadRes p a = (\<exists>y. ([y^2 = a] (mod p)))"
+
+definition Legendre :: "int \<Rightarrow> int \<Rightarrow> int" where
+ "Legendre a p = (if ([a = 0] (mod p)) then 0
+ else if QuadRes p a then 1
+ else -1)"
+
subsection \<open>A locale for residue rings\<close>
definition residue_ring :: "int \<Rightarrow> int ring"