lean_workbook_plus_81768

Proved

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

$\omega^{3}-1=0\implies (\omega-1)(\omega^{2}+\omega+1)=0$ . Since $\omega-1$ is not 0, $\omega^{2}+\omega+1=0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_81768  (ω : ℂ)
  (h₀ : ω^3 = 1)
  (h₁ : ω ≠ 1) :
  ω^2 + ω + 1 = 0   :=  by sorry

Source