English
Product of sums of two squares can be expressed as a sum of four squares with a specific sign pattern illustrating quaternionic multiplication.
Русский
Произведение сумм квадратов выражается как сумма четырех квадратов с определенной схемой знаков, демонстрирующей умножение кватернионов.
LaTeX
$$$(x_1^2+x_2^2+x_3^2+x_4^2)(y_1^2+y_2^2+y_3^2+y_4^2) = (x_1y_1 - x_2y_2 - x_3y_3 - x_4y_4)^2 + (x_1y_2 + x_2y_1 + x_3y_4 - x_4y_3)^2 + (x_1y_3 - x_2y_4 + x_3y_1 + x_4y_2)^2 + (x_1y_4 + x_2y_3 - x_3y_2 + x_4y_1)^2$$$
Lean4
/-- Brahmagupta-Fibonacci identity or Diophantus identity, see
<https://en.wikipedia.org/wiki/Brahmagupta%E2%80%93Fibonacci_identity>.
This sign choice here corresponds to the signs obtained by multiplying two complex numbers.
-/
theorem sq_add_sq_mul_sq_add_sq :
(x₁ ^ 2 + x₂ ^ 2) * (y₁ ^ 2 + y₂ ^ 2) = (x₁ * y₁ - x₂ * y₂) ^ 2 + (x₁ * y₂ + x₂ * y₁) ^ 2 := by ring
