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 (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 b x y u 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.mod_four_ne_three_of_mem_primeFactors_of_isSquare_neg_one {p n : ℕ} (hp : p ∈ n.primeFactors) (hs : IsSquare (-1)) : p % 4 ≠ 3

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

@[deprecated Nat.mod_four_ne_three_of_mem_primeFactors_of_isSquare_neg_one "Note that the statement now uses `Nat.primeFactors`, you can use `Nat.mem_primeFactors` to get the previous formulation" (since := "2025-10-15")]

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

Alias of Nat.mod_four_ne_three_of_mem_primeFactors_of_isSquare_neg_one.

---

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

theorem ZMod.isSquare_neg_one_iff_forall_mem_primeFactors_mod_four_ne_three {n : ℕ} (hn : Squarefree n) : IsSquare (-1) ↔ ∀ q ∈ n.primeFactors, q % 4 ≠ 3

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

@[deprecated ZMod.isSquare_neg_one_iff_forall_mem_primeFactors_mod_four_ne_three "Note that the statement now uses `Nat.primeFactors`, you can use `Nat.mem_primeFactors` and `Squarefree.ne_zero` to get the previous formulation" (since := "2025-10-15")]

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

Alias of ZMod.isSquare_neg_one_iff_forall_mem_primeFactors_mod_four_ne_three.

---

If n is a squarefree natural number, then -1 is a square modulo n if and only if n does not have a prime factor 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 ∈ n.primeFactors, 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.)

@[implicit_reducible]

instance instDecidableExistsNatEqHAddHPowOfNat_mathlib {n : ℕ} : Decidable (∃ (x : ℕ) (y : ℕ), n = x ^ 2 + y ^ 2)