Quadratic equations and functions

Compute the discriminant of $3x^2 - 5x + 2$.

Solve $x^2 - x - 12 = 0$. Enter the solutions as a set, for example {1, 2}.

How many different real roots does $4x^2 - 12x + 9$ have?

Kofi solves $x^2 = 3x$ by dividing both sides by $x$ and gets $x = 3$. What is wrong?

A goat pen is built against a straight wall using $60$ m of fencing for the other three sides. What is the largest possible area of the pen, in square metres?

Without solving, find the sum and the product of the roots of $2x^2 - 7x + 3 = 0$.

Find the positive number $k$ for which $x^2 + kx + 16 = 0$ has exactly one real root.

In Mathlib, Real.sqrt of a negative number is defined to be 0. The theorem Lumenary.Quadratics.quadratic_formula has the hypothesis hΔ : 0 ≤ b ^ 2 - 4 * a * c. What would happen if we deleted it?

Write real_roots(a, b, c) that returns the sorted list of the different real roots of $ax^2 + bx + c$ (with $a \ne 0$): two roots if $\Delta > 0$, one if $\Delta = 0$, and the empty list if $\Delta < 0$. Use math.sqrt.