mathlib3

44999a92 - feat(combinatorics/additive/behrend): Behrend's construction (#14070)

feat(combinatorics/additive/behrend): Behrend's construction (#14070) Construct large Salem-Spencer sets in `ℕ` using Behrend's construction. The idea is to turn the Euclidean sphere into a discrete set of points in Euclidean space which we then squash onto `ℕ`. Co-authored-by: Bhavik Mehta <bhavik.mehta8@gmail.com> Co-authored-by: Bhavik Mehta <bm489@cam.ac.uk>