mathlib documentation

number_theory.sum_four_squares

theorem int.sum_two_squares_of_two_mul_sum_two_squares {m x y : } :
2 * m = x ^ 2 + y ^ 2m = ((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