lean_workbook_plus_6482
ProvedFind the roots of the quadratic:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_6482 (x : ℝ) : 2.5 * x ^ 2 + 3 * x - 4 = 0 ↔ x = -2 ∨ x = 0.8 := by sorry
Source
Find the roots of the quadratic:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_6482 (x : ℝ) : 2.5 * x ^ 2 + 3 * x - 4 = 0 ↔ x = -2 ∨ x = 0.8 := by sorry