A finite sign-reversing bijection negates the total sum

Proved

ProofsInTheBook.Chapter30.sum_eq_neg_self_of_sign_reversing_equiv

by xiangyazi24 · Sep 12, 2026 · Mathlib c5ea003 (Lean v4.30.0)

combinatoricsconditional-identitydeterminantsfinite-sumslean4proofs-from-the-book

Let A be a finite type, let R be an additive commutative group, let $\tau:A\simeq A$ be a bijection, and let $w:A\to R$ satisfy $w(\tau x)=-w(x)$ for every x. Then

\sum_{x\in A}w(x)=-\sum_{x\in A}w(x).

Neither an involution condition on the bijection nor a torsion-free assumption on R is required. The conclusion alone does not force the sum to be zero in the presence of 2-torsion.

Preamble

import Mathlib
import Definitions.Def_ProofsInTheBook_Chapter30
open ProofsInTheBook.Chapter30
open Matrix BigOperators

Formal statement

theorem ProofsInTheBook.Chapter30.sum_eq_neg_self_of_sign_reversing_equiv {α R : Type*} [Fintype α]
    [AddCommGroup R] (τ : α ≃ α) (w : α → R) (hw : ∀ x, w (τ x) = -w x) :
    (∑ x : α, w x) = -∑ x : α, w x := by sorry

Source

Exact repository declaration: https://github.com/xiangyazi24/proof_in_the_book/blob/88d88d141768cded75e782c525ef1bf04b8fe220/ProofsInTheBook/Chapter30.lean#L52. PathCountSystem hypotheses: https://github.com/xiangyazi24/proof_in_the_book/blob/88d88d141768cded75e782c525ef1bf04b8fe220/ProofsInTheBook/Chapter30.lean#L435. Explicit scope limitation: https://github.com/xiangyazi24/proof_in_the_book/blob/88d88d141768cded75e782c525ef1bf04b8fe220/ProofsInTheBook/Chapter30.lean#L578. Repository topic: “Lattice paths and determinants.” No edition-specific chapter mapping or geometric application is asserted.

View graph