lean_workbook_plus_43204

Proved

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

$(2x - 1)(x - 2) = 0$ . So $x = \frac {1}{2}$ or $2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_43204  (x : ℝ)
  (h₀ : (2 * x - 1) * (x - 2) = 0) :
  x = 1 / 2 ∨ x = 2   :=  by sorry

Source