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.

source

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 #

source

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.

source

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 #

source

theorem zmod.is_square_neg_one_of_dvd {m n : ℕ} (hd : m ∣ n) (hs : is_square (-1)) :

is_square (-1)

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

source

theorem zmod.is_square_neg_one_mul {m n : ℕ} (hc : m.coprime n) (hm : is_square (-1)) (hn : is_square (-1)) :

is_square (-1)

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

source

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.

source

theorem zmod.is_square_neg_one_iff {n : ℕ} (hn : squarefree n) :

is_square (-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.

source

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 #

source

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.

source

theorem zmod.is_square_neg_one_of_eq_sq_add_sq_of_is_coprime {n x y : ℤ} (h : n = x ^ 2 + y ^ 2) (hc : is_coprime x y) :

is_square (-1)

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

source

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

is_square (-1)

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

source

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 #

source

theorem nat.eq_sq_add_sq_iff {n : ℕ} :

(∃ (x y : ℕ), n = x ^ 2 + y ^ 2) ↔ ∀ {q : ℕ}, nat.prime q → q % 4 = 3 → even (padic_val_nat 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 padic_val_nat q 0 = 0 by definition.)