mathlib3 documentation

number_theory.sum_four_squares

Lagrange's four square theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.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.exists_sq_add_sq_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

Four squares theorem