lean_workbook_plus_71695

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

And solutions $\boxed{x\in\left\{-\frac 32,-\frac 12\right\}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_71695  (x : ℝ)
  (h₀ : x^2 + 2 * x + 3 / 4 = 0) :
  x = -3 / 2 ∨ x = -1 / 2   :=  by sorry

Source