Existing in Mathlib · Combinatorics and number theory
Erdős–Ginzburg–Ziv Theorem
Assign a residue modulo n to every index in a finite set. If there are at least 2n−1 indices, then some n distinct indices carry values whose sum is zero modulo n. Different indices may carry the same residue.
- zero-sum subsequences
- cyclic groups
- indexed finite families
- Chevalley–Warning
- prime-composite induction
Exact theorem
Exact Mathlib statement
theorem ZMod.erdos_ginzburg_ziv {ι : Type*} {n : ℕ} {s : Finset ι} (a : ι → ZMod n) (hs : 2 * n - 1 ≤ #s) : ∃ t ⊆ s, #t = n ∧ ∑ i ∈ t, a i = 0The theorem at a glance
Erdős–Ginzburg–Ziv Theorem at a glance
A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.
Erdős–Ginzburg–Ziv Theorem at a glance
Detailed visual description
The poster places the exact lower-bound hypothesis, indexed selection, and ZMod n conclusion above a count-exact seven-ticket example. A source-anchored route ribbon names Chevalley–Warning for the prime case and disjoint-block factor induction for the composite case; the footer retains the at-least, n=0, uniqueness, and algorithm boundaries.
Statement structure
Statement and scope
Read the exact Mathlib declaration
This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.
Indexed residues converging to zero — Scientific schematic
Detailed visual description
Seven separate circular tokens represent indexed residues, so the repeated values remain distinct objects. Gold double outlines mark exactly the two 1 tokens and two 3 tokens, and exactly four gold arrows carry those selected values into a central zero with a fourfold modular-cycle motif. The unselected 2, 0, and 2 tokens have plain charcoal outlines and no connectors. This is the threshold-size n = 4 example; the theorem's hypothesis allows more than 2n−1 indices and does not assert uniqueness or an extraction algorithm.
Why it matters
A mathematical landmark
The Erdős–Ginzburg–Ziv theorem is a foundational zero-sum selection principle. Mathlib’s route also exposes a striking proof architecture: Chevalley–Warning supplies the prime case, while induction over prime and composite factors assembles disjoint zero-sum blocks for general n.
ProofAtlas record
What has been checked
Mathlib is the source of the theorem; the local Lean replay and page review are separate.
Claim boundary
No new theorem is claimed
This page indexes Mathlib’s finite indexed-family theorem in ZMod n. The hypothesis is 2*n−1 ≤ |s|, and the conclusion selects a subset t of exactly n distinct indices whose indexed values sum to zero. Values at different indices may repeat. The statement includes n=0 through the empty selection; it does not require exactly 2n−1 input indices, assert uniqueness, count witnesses, or provide an extraction algorithm.
- Proof Atlas did not originate the Erdős–Ginzburg–Ziv theorem or Mathlib’s declaration.
- The selected declaration is an indexed-family statement; it does not require the residue values themselves to be distinct.
- The hypothesis is a lower bound on the number of indices, not an exact-length requirement.
- The declaration does not assert uniqueness, count valid selections, or supply an extraction algorithm.
- The generated explanation and visuals are not proof evidence.
Source and local evidence
Where the theorem comes from
- Existing declaration
ZMod.erdos_ginzburg_zivin mathlib- Relationship
- The checked artifact is the upstream declaration itself
- Local Lean evidence
artifact.library.mathlib.erdos-ginzburg-ziv-theorem.v001