mathlib documentation

number_theory.sum_two_squares

Sums of two squares #

Proof of Fermat's theorem on the sum of two squares. Every prime congruent to 1 mod 4 is the sum of two squares.

Todo #

Fully characterize the natural numbers that are the sum of two squares: those such that for every prime p congruent to 3 mod 4, the largest power of p dividing them is even.

theorem nat.prime.sq_add_sq {p : } [fact (nat.prime p)] (hp : p % 4 = 1) :
∃ (a b : ), a ^ 2 + b ^ 2 = p

Fermat's theorem on the sum of two squares. Every prime congruent to 1 mod 4 is the sum of two squares. Also known as Fermat's Christmas theorem.