English
If p is a natural prime and p is not irreducible in ℤ[i], then there exist a,b ∈ ℤ with a^2 + b^2 = p.
Русский
Если p — натуральное простое число и p не является неразложимым в ℤ[i], то существуют a,b ∈ ℤ такие, что a^2 + b^2 = p.
LaTeX
$$$ \exists a,b \in \mathbb{Z}, \ a^2 + b^2 = p $$$
Lean4
theorem sq_add_sq_of_nat_prime_of_not_irreducible (p : ℕ) [hp : Fact p.Prime] (hpi : ¬Irreducible (p : ℤ[i])) :
∃ a b, a ^ 2 + b ^ 2 = p :=
have hpu : ¬IsUnit (p : ℤ[i]) :=
mt norm_eq_one_iff.2 <| by
rw [norm_natCast, Int.natAbs_mul, mul_eq_one]
exact fun h => (ne_of_lt hp.1.one_lt).symm h.1
have hab : ∃ a b, (p : ℤ[i]) = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b := by
simpa [irreducible_iff, hpu, not_forall, not_or] using hpi
let ⟨a, b, hpab, hau, hbu⟩ := hab
have hnap : (norm a).natAbs = p :=
((hp.1.mul_eq_prime_sq_iff (mt norm_eq_one_iff.1 hau) (mt norm_eq_one_iff.1 hbu)).1 <| by
rw [← Int.natCast_inj, Int.natCast_pow, sq, ← @norm_natCast (-1), hpab]; simp).1
⟨a.re.natAbs, a.im.natAbs, by simpa [natAbs_norm_eq, sq] using hnap⟩
