English
Over Z/pZ with p prime, every element can be written as a^2 + b^2 for some a,b in Z/pZ.
Русский
В ζMod p, где p — простое, каждый элемент можно представить как a^2 + b^2 (mod p).
LaTeX
$$$\\exists a,b \\in \\mathbb{Z}/p\\mathbb{Z},\\ a^2 + b^2 \\equiv x \\pmod p$ for every $x \\in \\mathbb{Z}/p\\mathbb{Z}$$$
Lean4
theorem sq_add_sq (p : ℕ) [hp : Fact p.Prime] (x : ZMod p) : ∃ a b : ZMod p, a ^ 2 + b ^ 2 = x :=
by
rcases hp.1.eq_two_or_odd with hp2 | hp_odd
· subst p
change Fin 2 at x
fin_cases x
· use 0; simp
· use 0, 1; simp
let f : (ZMod p)[X] := X ^ 2
let g : (ZMod p)[X] := X ^ 2 - C x
obtain ⟨a, b, hab⟩ : ∃ a b, f.eval a + g.eval b = 0 :=
@exists_root_sum_quadratic _ _ _ _ f g (degree_X_pow 2) (degree_X_pow_sub_C (by decide) _)
(by rw [ZMod.card, hp_odd])
refine ⟨a, b, ?_⟩
rw [← sub_eq_zero]
simpa only [f, g, eval_C, eval_X, eval_pow, eval_sub, ← add_sub_assoc] using hab
