English
For any a: ι → ZMod n and any finite s with |s| ≥ 2n − 1, there exists t ⊆ s with |t| = n such that the sum ∑_{i∈t} a(i) is congruent to 0 modulo n.
Русский
Для любой функции a:ι→ZMod n и любого конечного s с |s| ≥ 2n−1 существует подмножество t ⊆ s размера n such that сумма ∑ a(i) по i∈t эквивалентна 0 по модулю n.
LaTeX
$$$\\exists t \\subseteq s, |t| = n \\wedge \\sum_{i\\in t} a(i) = 0$ in ZMod n$$
Lean4
/-- The **Erdős–Ginzburg–Ziv theorem** for `ℤ/nℤ`.
Any sequence of at least `2 * n - 1` elements of `ZMod n` contains a subsequence of `n` elements
whose sum is zero. -/
theorem erdos_ginzburg_ziv (a : ι → ZMod n) (hs : 2 * n - 1 ≤ #s) : ∃ t ⊆ s, #t = n ∧ ∑ i ∈ t, a i = 0 := by
simpa [← ZMod.intCast_zmod_eq_zero_iff_dvd] using Int.erdos_ginzburg_ziv (ZMod.cast ∘ a) hs
