English
For any multiset s of elements of ZMod n with at least 2n−1 elements, there exists a submultiset t ≤ s with |t| = n whose sum is 0 in ZMod n.
Русский
Для мультимножества элементов ZMod n с не менее чем 2n−1 элементами найдётся подмультимножество t ⊆ s размера n, сумма которого равна 0 в ZMod n.
LaTeX
$$∃ t ≤ s, |t| = n ∧ t.sum = 0$$
Lean4
/-- 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`. -/
theorem erdos_ginzburg_ziv_multiset (s : Multiset (ZMod n)) (hs : 2 * n - 1 ≤ Multiset.card s) :
∃ t ≤ s, Multiset.card t = n ∧ t.sum = 0 :=
by
obtain ⟨t, hts, ht⟩ := ZMod.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⟩
