A negative discriminant excludes real roots
ProvedWorkbookSource.plus_41247lean-workbooksource-checked
Given and a negative discriminant, what can be said about the roots of the corresponding quadratic?
Source: InternLM Lean-Workbook, record lean_workbook_plus_41247 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.plus_41247 (a : ℝ) (b : ℝ) (c : ℝ) (ha : a > 0) (h : b^2 - 4*a*c < 0) : ¬ (∃ x, a*x^2 + b*x + c = 0) := by sorry
Source