lean_workbook_plus_33582
ProvedExplain why has real roots only when
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_33582 (b c : ℝ) : (∃ x, x^2 + b * x + c = 0) ↔ b^2 - 4*c >= 0 := by sorry
Source
Explain why has real roots only when
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_33582 (b c : ℝ) : (∃ x, x^2 + b * x + c = 0) ↔ b^2 - 4*c >= 0 := by sorry