# mathlib3documentation

number_theory.sum_two_squares

# Sums of two squares #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} [comm_ring R] {a b x y u v : R} (ha : a = x ^ 2 + y ^ 2) (hb : b = u ^ 2 + v ^ 2) :
(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.is_square_neg_one_of_dvd {m n : } (hd : m n) (hs : is_square (-1)) :

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

theorem zmod.is_square_neg_one_mul {m n : } (hc : m.coprime n) (hm : is_square (-1)) (hn : is_square (-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_is_square_neg_one {p n : } (hpp : nat.prime p) (hp : p n) (hs : is_square (-1)) :
p % 4 3

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

theorem zmod.is_square_neg_one_iff {n : } (hn : squarefree n) :
is_square (-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 is not divisible by a prime q such that q % 4 = 3.

theorem zmod.is_square_neg_one_iff' {n : } (hn : squarefree n) :
is_square (-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_is_square_mod_neg_one {n : } (h : is_square (-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.is_square_neg_one_of_eq_sq_add_sq_of_is_coprime {n x y : } (h : n = x ^ 2 + y ^ 2) (hc : y) :

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

theorem zmod.is_square_neg_one_of_eq_sq_add_sq_of_coprime {n x y : } (h : n = x ^ 2 + y ^ 2) (hc : x.coprime y) :

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 is_square (-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 = 3 even 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 padic_val_nat q 0 = 0 by definition.)