Olson: a zero-sum-free set has more than $1+\frac19|A|^2$ subset sums

Let $G$ be an abelian group and let $A \subseteq G$ be a finite, nonempty set of distinct elements which is zero-sum-free: no nonempty subset of $A$ sums to $0$. Write

for the set of all subset sums of $A$; the empty subset contributes the element $0$, so $0 \in \mathcal{P}(A)$ always. Then

This is a theorem of J. E. Olson, quoted as Theorem 7 by Erdős, Lev, Rauzy, Sándor and Sárközy. It is the engine behind every bound of the shape "a zero-sum-free set in a finite group is small": since $\mathcal{P}(A)$ is contained in $G$, the inequality immediately gives $|A| < 3\sqrt{|G|}$ for a zero-sum-free subset of a finite abelian group $G$. It is one of the two classical addition theorems on which the Erdős–Lev–Rauzy–Sándor–Sárközy bound $F(N) < 3\sqrt{N} + 1$ for non-dividing sets rests.

Formalization Note The set of subset sums is rendered as the image of the powerset of $A$ under the summation map, and the zero-sum-free hypothesis quantifies over members of A.powerset in the same style as the definition of NonDividing. Nonemptiness of $A$ is required: for $A = \emptyset$ both sides of the inequality equal $1$, so the strict inequality fails. No finiteness assumption on $G$ is imposed, matching the source, which states the result for an arbitrary abelian group.