English
As above, the classical Euler four-square identity for naturals: the product of two sums of four squares is itself a sum of four squares.
Русский
Как и выше, классическое Эйлерово тождество четырёх квадратов для натуральных чисел: произведение двух сумм четырёх квадратов снова является суммой четырёх квадратов.
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**, a version for natural numbers. -/
theorem euler_four_squares (a b c d x y z w : ℕ) :
((a : ℤ) * x - b * y - c * z - d * w).natAbs ^ 2 + ((a : ℤ) * y + b * x + c * w - d * z).natAbs ^ 2 +
((a : ℤ) * z - b * w + c * x + d * y).natAbs ^ 2 +
((a : ℤ) * w + b * z - c * y + d * x).natAbs ^ 2 =
(a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * (x ^ 2 + y ^ 2 + z ^ 2 + w ^ 2) :=
by
rw [← Int.natCast_inj]
push_cast
simp only [sq_abs, _root_.euler_four_squares]
