# Documentation

Mathlib.NumberTheory.SumFourSquares

# Lagrange's four square theorem #

The main result in this file is sum_four_squares, a proof that every natural number is the sum of four square numbers.

## Implementation Notes #

The proof used is close to Lagrange's original proof.

theorem euler_four_squares {R : Type u_1} [] (a : R) (b : R) (c : R) (d : R) (x : R) (y : R) (z : R) (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)

Euler's four-square identity.

theorem Nat.euler_four_squares (a : ) (b : ) (c : ) (d : ) (x : ) (y : ) (z : ) (w : ) :
Int.natAbs (a * x - b * y - c * z - d * w) ^ 2 + Int.natAbs (a * y + b * x + c * w - d * z) ^ 2 + Int.natAbs (a * z - b * w + c * x + d * y) ^ 2 + Int.natAbs (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)

Euler's four-square identity, a version for natural numbers.

theorem Int.sq_add_sq_of_two_mul_sq_add_sq {m : } {x : } {y : } (h : 2 * m = x ^ 2 + y ^ 2) :
m = ((x - y) / 2) ^ 2 + ((x + y) / 2) ^ 2
theorem Int.lt_of_sum_four_squares_eq_mul {a : } {b : } {c : } {d : } {k : } {m : } (h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = k * m) (ha : 2 * a < m) (hb : 2 * b < m) (hc : 2 * c < m) (hd : 2 * d < m) :
k < m
Lagrange's four squares theorem for a prime number. Use Nat.sum_four_squares instead.