English
If −1 is a square modulo n, then there exist integers x,y with n = x^2 + y^2.
Русский
Если −1 является квадратом по модулю n, то существуют целые x,y такие, что n = x^2 + y^2.
LaTeX
$$$ IsSquare(-1 : ZMod n) \Rightarrow \exists x,y \in \mathbb{N}, n = x^2 + y^2 $$$
Lean4
/-- If `-1` is a square modulo the natural number `n`, then `n` is a sum of two squares. -/
theorem eq_sq_add_sq_of_isSquare_mod_neg_one {n : ℕ} (h : IsSquare (-1 : ZMod n)) : ∃ x y : ℕ, n = x ^ 2 + y ^ 2 := by
induction n using induction_on_primes with
| zero => exact ⟨0, 0, rfl⟩
| one => exact ⟨0, 1, rfl⟩
| prime_mul p n hpp ih =>
haveI : Fact p.Prime := ⟨hpp⟩
have hp : IsSquare (-1 : ZMod p) := ZMod.isSquare_neg_one_of_dvd ⟨n, rfl⟩ h
obtain ⟨u, v, huv⟩ := Nat.Prime.sq_add_sq (ZMod.exists_sq_eq_neg_one_iff.mp hp)
obtain ⟨x, y, hxy⟩ := ih (ZMod.isSquare_neg_one_of_dvd ⟨p, mul_comm _ _⟩ h)
exact Nat.sq_add_sq_mul huv.symm hxy
