:: deftheorem defDCpq defines Discriminant FIELD_9:def 11 :
for R being non degenerated Ring
for p being monic purely_quadratic Polynomial of R
for b₃ being Element of R holds
( b₃ = Discriminant p iff ex c being Element of R st
( p = <%c,(0. R),(1. R)%> & b₃ = - (4 '*' c) ) );