lean_workbook_plus_66178

Proved

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

Find the roots of the equation $x^3+ax^2+bx+c=0$ given $-a = x_0+2\alpha$ , $+b=2\alpha x_0 + \alpha^2+\beta^2$ , and $-c = \left(\alpha^2+\beta^2\right)x_0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_66178 (a b c α β : ℂ) (x0 : ℂ) (h1 : -a = x0 + 2 * α) (h2 : b = 2 * α * x0 + α^2 + β^2) (h3 : -c = (α^2 + β^2) * x0) : x0^3 + a * x0^2 + b * x0 + c = 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph