Off-diagonal sums of a symmetric function

The off-diagonal sum of f : α → α → M over a finite set s is ∑ i ∈ s, ∑ j ∈ s.erase i, f i j: every ordered pair of distinct elements of s contributes once. When f is symmetric the two members of each unordered pair contribute equal terms, so the whole sum is even; this is Finset.even_sum_sum_erase, proved by induction on s.

Main results

• Finset.even_sum_sum_erase: the off-diagonal sum of a symmetric function over a finite set is even.

theorem Finset.even_sum_sum_erase {α : Type u_1} {M : Type u_2} [DecidableEq α] [AddCommMonoid M] {f : α → α → M} (s : Finset α) (hf : ∀ i ∈ s, ∀ j ∈ s, f i j = f j i) : Even (∑ i ∈ s, ∑ j ∈ s.erase i, f i j)

The off-diagonal sum of a symmetric function is even. The ordered pairs of distinct elements of s come in transposed couples contributing equal terms, so f need only be symmetric on s.