:: deftheorem Def3 defines Lege INT_5:def 3 :
for a being Integer
for p being Prime holds
( ( a is_quadratic_residue_mod p & a mod p <> 0 implies Lege (a,p) = 1 ) & ( a is_quadratic_residue_mod p & a mod p = 0 implies Lege (a,p) = 0 ) & ( ( not a is_quadratic_residue_mod p or not a mod p <> 0 ) & ( not a is_quadratic_residue_mod p or not a mod p = 0 ) implies Lege (a,p) = - 1 ) );