Sums of two squares

Fermat's theorem on the sum of two squares. Every prime p congruent to 1 mod 4 is the sum of two squares; see Nat.Prime.sq_add_sq (which has the weaker assumption p % 4 ≠ 3).

We also give the result that characterizes the (positive) natural numbers that are sums of two squares as those numbers n such that for every prime q congruent to 3 mod 4, the exponent of the largest power of q dividing n is even; see Nat.eq_sq_add_sq_iff.

There is an alternative characterization as the numbers of the form a^2 * b, where b is a natural number such that -1 is a square modulo b; see Nat.eq_sq_add_sq_iff_eq_sq_mul.

theorem Nat.Prime.sq_add_sq {p : ℕ} [Fact (Nat.Prime p)] (hp : p % 4 ≠ 3) : ∃ (a : ℕ) (b : ℕ), a ^ 2 + b ^ 2 = p

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

Generalities on sums of two squares

theorem sq_add_sq_mul {R : Type u_1} [CommRing R] {a : R} {b : R} {x : R} {y : R} {u : R} {v : R} (ha : a = x ^ 2 + y ^ 2) (hb : b = u ^ 2 + v ^ 2) : ∃ (r : R) (s : R), a * b = r ^ 2 + s ^ 2

The set of sums of two squares is closed under multiplication in any commutative ring. See also sq_add_sq_mul_sq_add_sq.

theorem Nat.sq_add_sq_mul {a : ℕ} {b : ℕ} {x : ℕ} {y : ℕ} {u : ℕ} {v : ℕ} (ha : a = x ^ 2 + y ^ 2) (hb : b = u ^ 2 + v ^ 2) : ∃ (r : ℕ) (s : ℕ), a * b = r ^ 2 + s ^ 2

The set of natural numbers that are sums of two squares is closed under multiplication.

Results on when -1 is a square modulo a natural number

theorem ZMod.isSquare_neg_one_of_dvd {m : ℕ} {n : ℕ} (hd : m ∣ n) (hs : IsSquare (-1)) : IsSquare (-1)

If -1 is a square modulo n and m divides n, then -1 is also a square modulo m.

theorem ZMod.isSquare_neg_one_mul {m : ℕ} {n : ℕ} (hc : m.Coprime n) (hm : IsSquare (-1)) (hn : IsSquare (-1)) : IsSquare (-1)

If -1 is a square modulo coprime natural numbers m and n, then -1 is also a square modulo m*n.

theorem Nat.Prime.mod_four_ne_three_of_dvd_isSquare_neg_one {p : ℕ} {n : ℕ} (hpp : Nat.Prime p) (hp : p ∣ n) (hs : IsSquare (-1)) : p % 4 ≠ 3

If a prime p divides n such that -1 is a square modulo n, then p % 4 ≠ 3.

theorem ZMod.isSquare_neg_one_iff {n : ℕ} (hn : Squarefree n) : IsSquare (-1) ↔ ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3

If n is a squarefree natural number, then -1 is a square modulo n if and only if n is not divisible by a prime q such that q % 4 = 3.

theorem ZMod.isSquare_neg_one_iff' {n : ℕ} (hn : Squarefree n) : IsSquare (-1) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3

If n is a squarefree natural number, then -1 is a square modulo n if and only if n has no divisor q that is ≡ 3 mod 4.

Relation to sums of two squares

theorem Nat.eq_sq_add_sq_of_isSquare_mod_neg_one {n : ℕ} (h : IsSquare (-1)) : ∃ (x : ℕ) (y : ℕ), n = x ^ 2 + y ^ 2

If -1 is a square modulo the natural number n, then n is a sum of two squares.

theorem ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_isCoprime {n : ℤ} {x : ℤ} {y : ℤ} (h : n = x ^ 2 + y ^ 2) (hc : IsCoprime x y) : IsSquare (-1)

If the integer n is a sum of two squares of coprime integers, then -1 is a square modulo n.

theorem ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_coprime {n : ℕ} {x : ℕ} {y : ℕ} (h : n = x ^ 2 + y ^ 2) (hc : x.Coprime y) : IsSquare (-1)

If the natural number n is a sum of two squares of coprime natural numbers, then -1 is a square modulo n.

theorem Nat.eq_sq_add_sq_iff_eq_sq_mul {n : ℕ} : (∃ (x : ℕ) (y : ℕ), n = x ^ 2 + y ^ 2) ↔ ∃ (a : ℕ) (b : ℕ), n = a ^ 2 * b ∧ IsSquare (-1)

A natural number n is a sum of two squares if and only if n = a^2 * b with natural numbers a and b such that -1 is a square modulo b.

Characterization in terms of the prime factorization

theorem Nat.eq_sq_add_sq_iff {n : ℕ} : (∃ (x : ℕ) (y : ℕ), n = x ^ 2 + y ^ 2) ↔ ∀ {q : ℕ}, Nat.Prime q → q % 4 = 3 → Even (padicValNat q n)

A (positive) natural number n is a sum of two squares if and only if the exponent of every prime q such that q % 4 = 3 in the prime factorization of n is even. (The assumption 0 < n is not present, since for n = 0, both sides are satisfied; the right hand side holds, since padicValNat q 0 = 0 by definition.)