refactor(sum_two_square): extract lemmas about primes in Z[i]

[ChrisHughes24]

This file extracts lemmas from the proof of Fermat's two square theorem.

I prove that a natural number is a prime in Z[i] iff it is three mod four. Fermat's two square theorem is a trivial consequences of this theorem and other theorems proved on the way to this theorem.

I also added docs to the Gaussian integer file.

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• reviewed and applied the documentation requirements
• for tactics:
  • added or adapted documentation in tactics.md
  • write an example of use of the new feature in tactics.lean
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

[robertylewis]

Thanks! This looks unobjectionable to me, but I'll leave it open a bit longer in case anyone else has comments.