lean_workbook_plus_53916

Proved

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

expanding and factorizing, this is just $(a+b)(b+c)(c+a) = 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_53916 {a b c : ℂ} : (a + b) * (b + c) * (c + a) = 0 ↔ a = -b ∨ b = -c ∨ c = -a   :=  by sorry

Source