lean_workbook_plus_25420

Proved

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

Let $w$ be a third root of unity that is not 1. Show that $w^5 + w + 1 = 0$ and use this to factor $x^5 + x + 1$ and $x^7 + x^2 + 1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_25420 (w : ℂ) (hw : w ^ 3 = 1) (hw' : w ≠ 1) : w ^ 5 + w + 1 = 0   :=  by sorry

Source