Theorems · Theorem · number theory

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

Defined in

Mathlib.NumberTheory.SumTwoSquares

Cited by

0 results in Mathlib

Foundations

Depth 153 from the axioms · uses propext, Classical.choice, Quot.sound