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

source
theorem nat.prime.sum_two_squares (p : ℕ) [hp : fact (nat.prime p)] (hp1 : 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