lean_workbook_plus_50874
ProvedFor to have real roots we need , whence .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_50874 : ∀ a : ℝ, (∃ x, x^2 - a*x + 2 = 0) → a^2 ≥ 8 := by sorry
Source
For to have real roots we need , whence .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_50874 : ∀ a : ℝ, (∃ x, x^2 - a*x + 2 = 0) → a^2 ≥ 8 := by sorry