lean_workbook_plus_32242

Proved

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

Given $z_1^3=z_2^3=z_3^3$ for distinct complex numbers $z_1$ , $z_2$ , $z_3$ , prove that $z_1+z_2+z_3=0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_32242 (z1 z2 z3 : ℂ) (hz1 : z1 ≠ z2) (hz2 : z1 ≠ z3) (hz3 : z2 ≠ z3) (h1 : z1 ^ 3 = z2 ^ 3) (h2 : z1 ^ 3 = z3 ^ 3) (h3 : z2 ^ 3 = z3 ^ 3) : z1 + z2 + z3 = 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph