by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
Euler's Four square Identity: (a2+b2+c2+d2)(w2+x2+y2+z2)=(aw+bx+cy+dz)2+(ax−bw+cz−dy)2+(ay−bz−cw+dx)2+(az+by−cx−dw)2
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_2165 (a b c d w x y z : ℝ) : (a^2+b^2+c^2+d^2)*(w^2+x^2+y^2+z^2) = (a*w+b*x+c*y+d*z)^2+(a*x-b*w+c*z-d*y)^2+(a*y-b*z-c*w+d*x)^2+(a*z+b*y-c*x-d*w)^2 := by sorry