lean_workbook_plus_23615

Proved

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

for any reals $x,y,z$ and $t$ we have the identity \n $x^4+y^4+z^4+t^4-4xyzt=(x-y)^2(x+y)^2+(z-t)^2(z+t)^2+2(xy-zt)^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_23615 (x y z t : ℝ) : x^4+y^4+z^4+t^4-4*x*y*z*t = (x-y)^2*(x+y)^2 + (z-t)^2*(z+t)^2 + 2*(x*y-z*t)^2   :=  by sorry

Source