lean_workbook_plus_17255

Proved

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

Prove that for a primitive third root of unity $\zeta$ , the sum $1+\zeta+\zeta^2$ equals 0.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_17255 (ζ : ℂ) (h : ζ ^ 3 = 1) (h' : ζ ≠ 1) : 1 + ζ + ζ ^ 2 = 0   :=  by sorry

Source