English
A product of two sums of four squares is a sum of four squares with explicit cross-terms.
Русский
Произведение двух сумм четырёх квадратов выражается как сумма четырёх квадратов с явными попарными слагаемыми.
LaTeX
$$As in the Brahmagupta–Fibonacci identity but for four squares: the product equals the sum of four squares with cross-terms as in the theorem.$$
Lean4
/-- Euler's four-square identity, see <https://en.wikipedia.org/wiki/Euler%27s_four-square_identity>.
This sign choice here corresponds to the signs obtained by multiplying two quaternions.
-/
theorem sum_four_sq_mul_sum_four_sq :
(x₁ ^ 2 + x₂ ^ 2 + x₃ ^ 2 + x₄ ^ 2) * (y₁ ^ 2 + y₂ ^ 2 + y₃ ^ 2 + y₄ ^ 2) =
(x₁ * y₁ - x₂ * y₂ - x₃ * y₃ - x₄ * y₄) ^ 2 + (x₁ * y₂ + x₂ * y₁ + x₃ * y₄ - x₄ * y₃) ^ 2 +
(x₁ * y₃ - x₂ * y₄ + x₃ * y₁ + x₄ * y₂) ^ 2 +
(x₁ * y₄ + x₂ * y₃ - x₃ * y₂ + x₄ * y₁) ^ 2 :=
by ring
