English
For any multiset s of integers with at least 2n−1 elements, there exists a submultiset t of s with |t| = n whose sum is divisible by n.
Русский
Для любого мультимножества целых с как минимум 2n−1 элементами существует подмультимножество t ⊆ s размера n, сумма которого делится на n.
LaTeX
$$∃ t ≤ s, |t| = n ∧ n ∣ t.sum$$
Lean4
/-- 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 erdos_ginzburg_ziv_multiset (s : Multiset ℤ) (hs : 2 * n - 1 ≤ Multiset.card s) :
∃ t ≤ s, Multiset.card t = n ∧ ↑n ∣ t.sum :=
by
obtain ⟨t, hts, ht⟩ := Int.erdos_ginzburg_ziv (s := s.toEnumFinset) Prod.fst (by simpa using hs)
exact ⟨t.1.map Prod.fst, Multiset.map_fst_le_of_subset_toEnumFinset hts, by simpa using ht⟩
