question about quadratic equations

Stream: Is there code for X?

[mathcat]

Hello, super new to lean, I have the quadratic equation hp : (6 - 4 * k) * x * x + (2 - 9 * k ^ 2) * x + (3 - k ^ 3) = 0, where x k : ℤ. The next step in my proof is to continue with a new hypothesis that the discriminant >= 0 if solutions exist. I looked through the docs, but I'm not able to use any of the discriminant theorems there. How do I continue?

[David Ang]

You might be able to find something in Algebra/QuadraticDiscriminant.lean

[Kevin Buzzard]

If you ask your question with a #mwe you're more likely to nerdsnipe people into solving it. I would multiply both sides of the equation by 4*(6-4k), rewrite as (2*(6-4k)*x+(2-9*k^2))^2=mess using ring/polyrith and deduce the result you need from squre>=0, i.e. I'd just complete the square manually because for me that would be quicker than looking in the library.

[mathcat]

okay will keep in mind, thanks a lot