lean_workbook_plus_35251

Proved

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

Given that $p + q + r = 0$ , prove the identity $pqr + (p+q)(q+r)(r+p) = -(p+q+r)^3$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_35251 (p q r : ℂ) (h : p + q + r = 0) :
  p*q*r + (p+q)*(q+r)*(r+p) = -(p+q+r)^3   :=  by sorry

Source