# Documentation

Mathlib.NumberTheory.SumTwoSquares

# 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 ()] (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} [] {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 s, 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)) :

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 : ) (hm : IsSquare (-1)) (hn : 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 : ) (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 : ) :
IsSquare (-1) ∀ {q : }, q nq % 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 : ) :
IsSquare (-1) ∀ {q : }, q nq % 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 : ) :

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 : ) :

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 : }, q % 4 = 3Even ()

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.)