lean_workbook_plus_8030

Proved

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

We have $x^2y+y^2z+z^2x=xy^2+yz^2+zx^2 \Leftrightarrow (x-y)(y-z)(z-x)=0$ . Thus, $x=y$ or $y=z$ or $z=x$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_8030 : ∀ x y z : ℝ, x^2*y + y^2*z + z^2*x = x*y^2 + y*z^2 + z*x^2 ↔ x = y ∨ y = z ∨ z = x   :=  by sorry

Source