Theorems · Theorem · number theory

Int.erdos_ginzburg_ziv

∀ {ι : Type u_1} {n : ℕ} {s : Finset ι} (a : ι → ℤ), 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.

Defined in

Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Cited by

2 results in Mathlib

Foundations

Depth 149 from the axioms · uses propext, Classical.choice, Quot.sound