Commit 2023-06-01 20:20 34ebaffc
View on Github →feat(number_theory/sum_two_squares): add result for general n (#19054)
This PR resolves the "Todo" that was left in number_theory.sum_two_squares
, i.e., it adds the result that characterizes natural numbers that are sums of two squares in terms of their prime factorization:
lemma nat.eq_sq_add_sq_iff {n : ℕ} :
(∃ x y : ℕ, n = x ^ 2 + y ^ 2) ↔
∀ {q : ℕ} (hq : q.prime) (h : q % 4 = 3), even (padic_val_nat q n) := ...
There is some discussion on Zulip regarding how to spell out the condition on the right hand side.