Commit 2023-06-01 20:20 34ebaffc

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.