The Erdős–Ginzburg–Ziv theorem

This file proves 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.

Main declarations

• Int.erdos_ginzburg_ziv: The Erdős–Ginzburg–Ziv theorem stated using sequences in ℤ
• ZMod.erdos_ginzburg_ziv: The Erdős–Ginzburg–Ziv theorem stated using sequences in ZMod n

theorem Int.erdos_ginzburg_ziv {ι : Type u_1} {n : ℕ} {s : Finset ι} (a : ι → ℤ) (hs : 2 * n - 1 ≤ s.card) : ∃ t ⊆ s, t.card = n ∧ ↑n ∣ ∑ i ∈ t, a i

The Erdős–Ginzburg–Ziv theorem for ℤ.

Any sequence of at least 2 * n - 1 elements of ℤ contains a subsequence of n elements whose sum is divisible by n.

theorem ZMod.erdos_ginzburg_ziv {ι : Type u_1} {n : ℕ} {s : Finset ι} (a : ι → ZMod n) (hs : 2 * n - 1 ≤ s.card) : ∃ t ⊆ s, t.card = n ∧ ∑ i ∈ t, a i = 0

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 Int.erdos_ginzburg_ziv_multiset {n : ℕ} (s : Multiset ℤ) (hs : 2 * n - 1 ≤ Multiset.card s) : ∃ t ≤ s, Multiset.card t = n ∧ ↑n ∣ t.sum

The Erdős–Ginzburg–Ziv theorem for ℤ for multiset.

Any multiset of at least 2 * n - 1 elements of ℤ contains a submultiset of n elements whose sum is divisible by n.

theorem ZMod.erdos_ginzburg_ziv_multiset {n : ℕ} (s : Multiset (ZMod n)) (hs : 2 * n - 1 ≤ Multiset.card s) : ∃ t ≤ s, Multiset.card t = n ∧ t.sum = 0

The Erdős–Ginzburg–Ziv theorem for ℤ/nℤ for multiset.

Any multiset of at least 2 * n - 1 elements of ℤ contains a submultiset of n elements whose sum is divisible by n.