This completed file is a regression example, not the paper's Theorem 1.2. It proves the classical one-dimensional Erdős--Ginzburg--Ziv theorem already supported by Mathlib.

def PrimeEGZ.HasZeroSumSubsequence {ι : Type} (p : ℕ) (a : ι → ZMod p) : Prop

A sequence a contains p terms, at distinct positions, whose sum is zero in ZMod p.

Equations

• PrimeEGZ.HasZeroSumSubsequence p a = ∃ (t : Finset ι), t.card = p ∧ ∑ i ∈ t, a i = 0

def PrimeEGZ.ForcesZeroSum (p N : ℕ) : Prop

Every sequence of length at least N in ZMod p contains a zero-sum subsequence of length p.

The index type is allowed to be an arbitrary finite type; this avoids making the definition depend on a particular enumeration of the sequence.

Equations

• PrimeEGZ.ForcesZeroSum p N = ∀ {ι : Type} [inst : Fintype ι] (a : ι → ZMod p), N ≤ Fintype.card ι → PrimeEGZ.HasZeroSumSubsequence p a

theorem PrimeEGZ.ForcesZeroSum.mono {p N M : ℕ} (h : ForcesZeroSum p N) (hNM : N ≤ M) : ForcesZeroSum p M

theorem PrimeEGZ.forcesZeroSum_two_mul_sub_one (p : ℕ) : ForcesZeroSum p (2 * p - 1)

The upper bound in the Erdős--Ginzburg--Ziv theorem.

Mathlib contains the stronger theorem ZMod.erdos_ginzburg_ziv, valid for every modulus, not only a prime modulus.

theorem PrimeEGZ.exists_forcing_length (p : ℕ) : ∃ (N : ℕ), ForcesZeroSum p N

noncomputable def PrimeEGZ.sFp (p : ℕ) : ℕ

The Erdős--Ginzburg--Ziv constant of ZMod p: the least length which forces a zero-sum subsequence of length p.

Equations

• PrimeEGZ.sFp p = Nat.find ⋯

theorem PrimeEGZ.sFp_spec (p : ℕ) : ForcesZeroSum p (sFp p)

theorem PrimeEGZ.sFp_min {p N : ℕ} (hN : ForcesZeroSum p N) : sFp p ≤ N

theorem PrimeEGZ.not_forcesZeroSum_two_mul_sub_two {p : ℕ} (hp : 2 ≤ p) : ¬ForcesZeroSum p (2 * p - 2)

The usual sharpness example: p - 1 zeroes and p - 1 ones do not contain a zero-sum subsequence of length p.

The positions are represented by Fin (p - 1) × Bool; the Boolean coordinate records whether the term is zero or one.

theorem PrimeEGZ.sFp_eq_two_mul_sub_one {p : ℕ} (hp : 2 ≤ p) : sFp p = 2 * p - 1

Sharp Erdős--Ginzburg--Ziv theorem. The proof actually works for every modulus p ≥ 2; the prime case is stated separately below.

theorem PrimeEGZ.erdos_ginzburg_ziv_prime {p : ℕ} (hp : Nat.Prime p) : sFp p = 2 * p - 1

The Erdős--Ginzburg--Ziv theorem for the prime field 𝔽_p = ZMod p: s(𝔽_p) = 2p - 1.