English
If a ≠ 0 and a x^2 + b x + c > 0 for all x, then discrim a b c < 0.
Русский
Если a ≠ 0 и a x^2 + b x + c > 0 для всех x, тогда дискриминант меньше 0.
LaTeX
$$$\mathrm{discrim}(a,b,c) < 0$$$
Lean4
/-- If a polynomial of degree 2 is always positive, then its discriminant is negative,
at least when the coefficient of the quadratic term is nonzero.
-/
theorem discrim_lt_zero (ha : a ≠ 0) (h : ∀ x : K, 0 < a * (x * x) + b * x + c) : discrim a b c < 0 :=
by
have : ∀ x : K, 0 ≤ a * (x * x) + b * x + c := fun x => le_of_lt (h x)
refine lt_of_le_of_ne (discrim_le_zero this) fun h' ↦ ?_
have := h (-b / (2 * a))
have : a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0 := by
rw [mul_assoc, quadratic_eq_zero_iff_of_discrim_eq_zero ha h' (-b / (2 * a))]
linarith
