[Merged by Bors] - feat(NumberTheory/SumTwoSquares): it is decidable whether a number is the sum of two squares#30273

SnirBroshi wants to merge 6 commits intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

SnirBroshi:feature/sum-of-two-squares-decidableSnirBroshi/mathlib4:feature/sum-of-two-squares-decidableCopy head branch name to clipboard