Is there a name for this identity involving series?

Question

I'm working through Spivak's Calculus, and for one of the problems I had to prove the Scharwz inequality. I derived this identity, and was wondering if this had a name, it seemed quite important. It's factoring the first sums into to squared terms:

$$\sum_{i=1}^{n}x_i^2\sum_{i=1}^{n}y_i^2 \equiv \left (\sum_{i=1}^{n}x_i y_i\right)^2 + \sum_{i=1}^{n-1}\left(\sum_{j=i+1}^{n}(x_i y_j - x_j y_i)^2 \right)$$

Here's an example when $n = 4$, because the identity is a bit unnerving, at least to me:

$$(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_1 y_1 + x_2 y_2 + x_3 y_3 + x_4 y_4)^2 + (x_1 y_2 - x_2 y_1)^2 + (x_1 y_3 - x_3 y_1)^2 + (x_1 y_4 - x_4 y_1)^2 \\ + (x_2 y_3 - x_3 y_2)^2 + (x_2 y_4 - x_4 y_2)^2 \\ + (x_3 y_4 - x_4 y_3)^2$$

Thanks.

Answer 1

This is called Lagrange's identity.

Answer 2

The special case $n=4$ that you gave is Euler's Four Square Identity.

The version given in the above link is not quite the same as the one you quote. In fact the one you quote is Euler's original Four Square Identity. It plays a crucial role in the proof that every positive integer is the sum of four squares. The modified version of the link (which is obtained simply by changing the sign of $x_1$) fits in better with the use of the identity to show that the norm of a product of two quaternions is the product of the norms.