:: deftheorem defines Disc EC_PF_1:def 7 :
for p being Prime
for a, b, b₄ being Element of (GF p) holds
( b₄ = Disc (a,b,p) iff for g4, g27 being Element of (GF p) st g4 = 4 mod p & g27 = 27 mod p holds
b₄ = (g4 * (a |^ 3)) + (g27 * (b |^ 2)) );