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

∃ (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