Restricted sumsets

This file defines the restricted sumset $S \hat{+} S$ for a finite set $S$.

def Finset.restrictedSumset {α : Type u_1} [Add α] [DecidableEq α] (S : Finset α) : Finset α

The restricted sumset of a set $S$, denoted $S \hat{+} S$, is the set $\lbrace s_1 + s_2 : s_1, s_2 \in S, s_1 \neq s_2 \rbrace$.

Equations

• S.restrictedSumset = Finset.image (fun (p : α × α) => p.1 + p.2) S.offDiag