Erdos-Ginzburg-Ziv

We formalize the Erdős–Ginzburg–Ziv theorem for integer multisets: every multiset of at least 2n−1 integers contains a submultiset of cardinality n whose sum is divisible by n. The proof is split into a prime-modulus argument over residue multisets and a strong-induction argument for the general case, following the classical theorem of Erdős, Ginzburg, and Ziv [1]. AI assistance was used for proof engineering. The final definitions, statements, and proofs are checked by Isabelle.