:: deftheorem defDC defines Discriminant FIELD_9:def 9 :
for R being non degenerated Ring
for p being quadratic Polynomial of R
for b₃ being Element of R holds
( b₃ = Discriminant p iff ex a being non zero Element of R ex b, c being Element of R st
( p = <%c,b,a%> & b₃ = (b ^2) - ((4 '*' a) * c) ) );