lean_workbook_plus_19487

Proved

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

Show that for all real numbers $x,y,z$ such that $x + y + z = 0$ and $xy + yz + zx = -3$ , the expression $x^3y + y^3z + z^3x$ is a constant.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_19487 (x y z : ℝ) (h1 : x + y + z = 0) (h2 : x*y + y*z + z*x = -3) : x^3*y + y^3*z + z^3*x = -9   :=  by sorry

Source