Email Gateway (Aug 18 2022 at 14:55): Email Gateway (Aug 18 2022 at 14:55):From: Tim McKenzie <tjm1983@gmail.com>
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
<><
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC