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