Erdős problem 541
Let be (not necessarily distinct) residues modulo a prime , such that there exists some so that if is non-empty and then .
Sources
FormalConjectures/ErdosProblems/
541.lean
Retained formal statement
Gao, Hamidoune, and Wang [GHW10] solved this for all moduli p (not necessarily prime).
∀ (p : ℕ) (a : Fin p → ZMod p), (∃ r, ∀ (S : Finset (Fin p)), S ≠ ∅ → ∑ i ∈ S, a i = 0 → S.card = r) → (Set.range a).ncard ≤ 2SolvedStatement only, no proof