Commit 2026-02-06 12:50 0431cf12

feat: add ComplexShape.EulerCharSigns for generalized Euler characteristic (#31121) Add ComplexShape.EulerCharSigns typeclass providing the alternating signs χ : ι → ℤˣ for Euler characteristic computations. Instances are provided for up ℕ, down ℕ, up ℤ, and down ℤ. The Euler characteristic definition (eulerChar) uses finsum to sum over all indices, with the ComplexShape as an explicit parameter. This allows working with arbitrary index types without requiring a Fintype instance, defaulting to 0 when the support is infinite. The GradedObject version is the primary definition, with HomologicalComplex.eulerChar and HomologicalComplex.homologyEulerChar as abbreviations that apply the graded object version to C.X and C.homology respectively. Split from #29713 as suggested by @joelriou.