Erdős Problem 476

References:

• erdosproblems.com/476
• [Er65b] Erdős, Paul, Some recent advances and current problems in number theory. Lectures on Modern Mathematics, Vol. III (1965), 196-244.
• [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).
• [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437.
• [dSHa94] Dias da Silva, J. A. and Hamidoune, Y. O., Cyclic spaces for Grassmann derivatives and additive theory. Bull. London Math. Soc. (1994), 140-146.

theorem Erdos476.erdos_476 : True ↔ ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (A : Finset (ZMod p)), A.restrictedSumset.card ≥ min (2 * A.card - 3) p

Let $A\subseteq \mathbb{F}_p$. Let [ A\hat{+}A = { a+b : a\neq b \in A}. ] Is it true that [ \lvert A\hat{+}A\rvert \geq \min(2\lvert A\rvert-3,p)? ]

This is the Erdős-Heilbronn inequality, proved by Dias da Silva and Hamidoune.