English
Euler's four-square identity holds for natural numbers: the sum of four squares of linear forms in a,b,c,d,x,y,z,w equals the product of the sums of squares of (a,b,c,d) and (x,y,z,w).
Русский
Эйлерово тождество четырёх квадратов выполняется для натуральных чисел: сумма квадратов четырёх линейных форм эквивалентна произведению сум квадратов двух троек.
LaTeX
$$$ (a^2+b^2+c^2+d^2)(x^2+y^2+z^2+w^2) = (ax-by-cz-dw)^2 + (ay+bx+dw-cz)^2 + (az-bw+cx+dy)^2 + (aw+bz-cy+dx)^2 $$$
Lean4
/-- **Euler's four-square identity**. -/
theorem euler_four_squares {R : Type*} [CommRing R] (a b c d x y z w : R) :
(a * x - b * y - c * z - d * w) ^ 2 + (a * y + b * x + c * w - d * z) ^ 2 + (a * z - b * w + c * x + d * y) ^ 2 +
(a * w + b * z - c * y + d * x) ^ 2 =
(a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * (x ^ 2 + y ^ 2 + z ^ 2 + w ^ 2) :=
by ring
