Positive and negative parts of a balanced sum

When a finite sum in a linearly ordered additive commutative group is zero, its total negative part equals its total positive part. This expresses the balance of supply and demand without requiring multiplication, an Archimedean property, or order completeness.

theorem Finset.sum_max_neg_eq_sum_max {ι : Type u_1} {K : Type u_2} [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] (s : Finset ι) (b : ι → K) (hb : ∑ v ∈ s, b v = 0) : ∑ v ∈ s, max (-b v) 0 = ∑ v ∈ s, max (b v) 0

A balanced finite family has equal total negative and positive parts.