PR #29713: Euler-Poincaré formula

Stream: PR reviews

[Jesse Alama]

I've opened PR #29713 adding the Euler-Poincaré formula to Mathlib. This adds the Euler characteristic for chain complexes (ChainComplex.eulerChar and ChainComplex.homologyEulerChar) and proves that the alternating sum of chain dimensions equals the alternating sum of homology dimensions for bounded complexes of finite-dimensional modules over a division ring. Any feedback welcome!

[Christian Merten]

For reference: There is already a discussion at #PR reviews > #29639.

[Jesse Alama]

Christian Merten said:

For reference: There is already a discussion at #PR reviews > #29639.

Thanks! I'm currently wondering if I should close that PR, for now, to focus on #29713. I'd base the Euler polyhedron formula work on top of #29713, so in that sense you could consider it still open, but I think it's a bit of noise/spam to keep that open, even as a draft.