:: deftheorem Def5 defines Lege_p EC_PF_1:def 5 :
for p being Prime
for a being Element of (GF p) holds
( ( a = 0 implies Lege_p a = 0 ) & ( a is quadratic_residue implies Lege_p a = 1 ) & ( not a = 0 & not a is quadratic_residue implies Lege_p a = - 1 ) );