English
A natural number n is a sum of two squares iff for every prime q with q ≡ 3 (mod 4), the exponent of q in n is even.
Русский
Число n является суммой двух квадратов тогда и только тогда, когда для каждого простого q, удовлетворяющего q ≡ 3 (mod 4), показатель степени q в факторизации n чётен.
LaTeX
$$$n=\\prod q^{e_q} \\quad\\Rightarrow\\quad \\forall q\\text{ prime},\\ q\\equiv 3\\ (4),\\ e_q\\text{ чётно}$ ⇔ (\\exists x,y, n=x^2+y^2).$$$
Lean4
/-- 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`. -/
theorem eq_sq_add_sq_iff_eq_sq_mul {n : ℕ} :
(∃ x y : ℕ, n = x ^ 2 + y ^ 2) ↔ ∃ a b : ℕ, n = a ^ 2 * b ∧ IsSquare (-1 : ZMod b) :=
by
constructor
· rintro ⟨x, y, h⟩
by_cases hxy : x = 0 ∧ y = 0
·
exact
⟨0, 1, by rw [h, hxy.1, hxy.2, zero_pow two_ne_zero, add_zero, zero_mul],
⟨0, by rw [zero_mul, neg_eq_zero, Fin.one_eq_zero_iff]⟩⟩
· have hg := Nat.pos_of_ne_zero (mt Nat.gcd_eq_zero_iff.mp hxy)
obtain ⟨g, x₁, y₁, _, h₂, h₃, h₄⟩ := Nat.exists_coprime' hg
exact ⟨g, x₁ ^ 2 + y₁ ^ 2, by rw [h, h₃, h₄]; ring, ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_coprime rfl h₂⟩
· rintro ⟨a, b, h₁, h₂⟩
obtain ⟨x', y', h⟩ := Nat.eq_sq_add_sq_of_isSquare_mod_neg_one h₂
exact ⟨a * x', a * y', by rw [h₁, h]; ring⟩
