mathlib

594e8848 - feat(combinatorics/additive/behrend): Behrend's lower bound on Roth numbers (#15327)

feat(combinatorics/additive/behrend): Behrend's lower bound on Roth numbers (#15327) This proves the explicit bound on Roth's numbers of the form `n / exp (O (sqrt (log n)))`. Co-authored-by: Bhavik Mehta <bmehta8@gmail.com>