lean_workbook_plus_32215

Proved

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

So $x^3+1 = 2x\Rightarrow x^3-2x+1=0\Rightarrow (x-1)\cdot \left(x^2+x-1\right) = 0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_32215  (x : ℝ)
  (h₀ : x^3 + 1 = 2 * x) :
  x^3 - 2 * x + 1 = 0   :=  by sorry

Source