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} [CommRing R] (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 : ) :
(a * x - b * y - c * z - d * w).natAbs ^ 2 + (a * y + b * x + c * w - d * z).natAbs ^ 2 + (a * z - b * w + c * x + d * y).natAbs ^ 2 + (a * w + b * z - c * y + d * x).natAbs ^ 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
theorem Int.exists_sq_add_sq_add_one_eq_mul (p : ) [hp : Fact (Nat.Prime p)] :
∃ (a : ) (b : ) (k : ), 0 < k k < p a ^ 2 + b ^ 2 + 1 = k * p
theorem Nat.Prime.sum_four_squares {p : } (hp : Nat.Prime p) :
∃ (a : ) (b : ) (c : ) (d : ), a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p

Lagrange's four squares theorem for a prime number. Use Nat.sum_four_squares instead.

theorem Nat.sum_four_squares (n : ) :
∃ (a : ) (b : ) (c : ) (d : ), a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n

Four squares theorem