mathlib documentation

number_theory.sum_four_squares

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 int.sum_two_squares_of_two_mul_sum_two_squares {m x y : } (h : 2 * m = x ^ 2 + y ^ 2) :
m = ((x - y) / 2) ^ 2 + ((x + y) / 2) ^ 2
theorem int.exists_sum_two_squares_add_one_eq_k (p : ) [hp : fact (nat.prime p)] :
∃ (a b : ) (k : ), a ^ 2 + b ^ 2 + 1 = (k) * p k < p
theorem nat.sum_four_squares (n : ) :
∃ (a b c d : ), a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n