mathlib3

34ebaffc - feat(number_theory/sum_two_squares): add result for general n (#19054)

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: ```lean 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](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Preferred.20spelling.20of.20p-adic.20valuation.3F/near/359896021) regarding how to spell out the condition on the right hand side. Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>