[isabelle] Discriminant

Working with Isabelle/HOL, I anticipate that in the near future 
I'm likely to need to use results about the number of real roots 
of a quadratic, which can be discerned from the discriminant.  Is 
there existing work in Isabelle/HOL on this?

The closest I can find is Fundamental_Theorem_Algebra.thy in the 
Library, which I might be able to use to establish that there are 
at most two real roots of a quadratic.  However, at first glance, 
it appears to be all about complex polynomials, so I'd need to 
massage its results into telling me about real quadratics.  I'm 
inclined to think that it might be easier for me to prove the 
results about real quadratics from scratch, by completing the 

I don't expect I'll immediately need any more general results 
about discriminants of polynomials of higher degree, but (of 
course) I'd be happy to use general results if someone's already 
proven them.


Attachment: signature.asc
Description: This is a digitally signed message part.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.