lean_workbook_plus_12950

Proved

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

Find the roots of the equation $x(x^2+8x+16)(4-x)=0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_12950 (x : ℝ) : x * (x^2 + 8 * x + 16) * (4 - x) = 0 ↔ x = 0 ∨ x = -4 ∨ x = 4   :=  by sorry

Source