[Merged by Bors] - feat: Zagier's "one-sentence proof" of Fermat's theorem on sums of two squares

[Parcly-Taxel]

---

[tb65536]

Here's a nice golf using Function.fixedPoints that avoids powers: zagier...zagier_golf

[Parcly-Taxel]

Here's a nice golf using Function.fixedPoints that avoids powers: zagier...zagier_golf

What a fantastic golf.

[ocfnash]

This is very nice but I suggest it would be be better placed in the archive folder, since we already have the result.

[Parcly-Taxel]

This is very nice but I suggest it would be be better placed in the archive folder, since we already have the result.

Done.

[mcdoll]

Could you please squeeze all of your nonterminal simps and add a bit more documentation in the proofs?

[ocfnash]

The naming in Archive/ZagierTwoSquares is not what we would use in Mathlib proper (it's semantic rather than based on type) but as this is going in the archive, I think we can leave it as it is.

Thanks!

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style