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

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

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 qq 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 : Squarefree n) :
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 : IsCoprime x y) :

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

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 qq % 4 = 3Even (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.)