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 square. 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. Tim <><
Description: This is a digitally signed message part.