lean_workbook_plus_25942

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Erdos-Ginzburg-Ziv Theorem: For any set of $2n-1$ positive integers, there exists $n$ positive integers in the set such that the sum of these positive integers is divisible by $n$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_25942 (n : ℕ) (A : Finset ℕ) (hA : A.card = 2 * n - 1) :
    ∃ B : Finset ℕ, B ⊆ A ∧ n ∣ B.sum (fun x ↦ x)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph