Commit 2024-07-28 16:06 07ede504

feat: The Erdős–Ginzburg–Ziv theorem (#14000) Prove the Erdős–Ginzburg–Ziv theorem as a corollary of Chevalley-Warning. This theorem states that among any (not necessarily distinct) 2 * n - 1 elements of ZMod n, we can find n elements of sum zero.