lean_workbook_plus_8578

Proved

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

当 $w^3=0$ 时，取 $y=1$ ， $z=0$ ，证明不等式 $(x-1)^2(x+1)^2(x^2-x+1)\geq0$ 成立。

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_8578 (x y z w : ℝ) (h₁ : w^3 = 0) (h₂ : y = 1) (h₃ : z = 0) : (x - 1)^2 * (x + 1)^2 * (x^2 - x + 1) ≥ 0   :=  by sorry

Source