lean_workbook_plus_59589
ProvedSolve the equation for in the interval .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_59589 (x : ℝ) (hx : -1 ≤ x ∧ x ≤ 1) : -3 * x ^ 2 - 3 * x + 3 / 2 = 0 ↔ x = -1 / 2 + Real.sqrt 3 / 2 ∨ x = -1 / 2 - Real.sqrt 3 / 2 := by sorry
Source