English
For a prime p, and x ∈ Z, there exist a,b ∈ N with a ≤ p/2, b ≤ p/2 such that a^2 + b^2 ≡ x (mod p).
Русский
Для простого p существует пара a,b ∈ N с ограничениями a ≤ p/2, b ≤ p/2 such that a^2 + b^2 ≡ x (mod p).
LaTeX
$$$\\exists a,b \\in \\mathbb{N},\\ a \\le \\frac{p}{2} \\land b \\le \\frac{p}{2} \\land a^2 + b^2 \\equiv x \\pmod p$$$
Lean4
/-- If `p` is a prime natural number and `x` is an integer number, then there exist natural numbers
`a ≤ p / 2` and `b ≤ p / 2` such that `a ^ 2 + b ^ 2 ≡ x [ZMOD p]`. This is a version of
`ZMod.sq_add_sq` with estimates on `a` and `b`. -/
theorem sq_add_sq_zmodEq (p : ℕ) [Fact p.Prime] (x : ℤ) :
∃ a b : ℕ, a ≤ p / 2 ∧ b ≤ p / 2 ∧ (a : ℤ) ^ 2 + (b : ℤ) ^ 2 ≡ x [ZMOD p] :=
by
rcases ZMod.sq_add_sq p x with ⟨a, b, hx⟩
refine ⟨a.valMinAbs.natAbs, b.valMinAbs.natAbs, ZMod.natAbs_valMinAbs_le _, ZMod.natAbs_valMinAbs_le _, ?_⟩
rw [← a.coe_valMinAbs, ← b.coe_valMinAbs] at hx
push_cast
rw [sq_abs, sq_abs, ← ZMod.intCast_eq_intCast_iff]
exact mod_cast hx
