Proof of `Parity of the Euler characteristic in odd dimension, and integrality for surfaces` (4th statement)

groundedproofs/Lax894236Proofs/Parity.lean · lax-894236

What this proof establishes

no assumptions

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

In ZMod2ZMod 2 every power djd^j with j1j ≥ 1 equals dd, so χχ reduces to dd times the sum of the binomial coefficients from the quadratic term on, which is 2(n+2)(n+3)2^(n+2) − (n+3): even when nn is odd.