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
This was proved by Erdős and Szemerédi [ErSz76] for p sufficiently large.
∀ᶠ (p : ℕ) in Filter.atTop, Nat.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