:: deftheorem defines not_quadratic_residue EC_PF_1:def 4 :
for p being Prime
for a being Element of (GF p) holds
( a is not_quadratic_residue iff ( a <> 0 & ( for x being Element of (GF p) holds not x |^ 2 = a ) ) );