- Rename eulerChar to boundedEulerChar for finite sums (0 to n-1)
- Add new eulerChar as infinite sum over all naturals
- Add boundedEulerChar_zero lemma for empty sum case
- Add boundedEulerChar_succ lemma for induction step
- Add theorem stating equivalence when modules eventually vanish (with sorry)

Based on feedback from PR leanprover-community#29646

This PR adds the Euler-Poincaré formula for bounded chain complexes of finite-dimensional vector spaces over a field, following feedback from @joelriou in leanprover-community#29639.

The main result states that for a bounded complex C that vanishes after position n:
∑_{i=0}^n (-1)^i dim(C_i) = ∑_{i=0}^n (-1)^i dim(H_i)

This builds upon the Euler characteristic definitions from leanprover-community#29646.

Key additions:
- Basic lemmas about chain complex differentials at boundaries (dFrom 0, dTo n)
- Relationship between dTo/dFrom and the underlying differentials
- General telescoping lemma for alternating sums
- The rank-nullity decomposition for chain complexes
- The main Euler-Poincaré theorem

Thanks to @joelriou for the valuable feedback that guided this implementation.

Co-authored-by: joelriou <joelriou@users.noreply.github.com>

Adopt the exact EulerCharacteristic.lean file from PR leanprover-community#29646
to maintain consistency. This file defines the Euler characteristic
of chain complexes with both bounded and infinite sum versions.

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>

Add the homological Euler characteristic definition needed for
the Euler-Poincaré formula. This matches the structure from PR leanprover-community#29646
while including the necessary definitions for our proof.

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>

Add the Euler-Poincaré formula proving that for bounded complexes of
finite-dimensional vector spaces, the alternating sum of dimensions
equals the alternating sum of homology dimensions.

This PR adds:
- `EulerCharacteristic.lean`: Defines Euler characteristic for chain complexes
  (adopted from PR leanprover-community#29646)
- `EulerPoincare.lean`: Proves the Euler-Poincaré formula
- Helper lemmas in `HomologicalComplex.lean` for bounded complexes

The main theorem shows that for a bounded complex C of finite-dimensional
vector spaces over a field k, if C vanishes after position n, then:
∑_{i=0}^n (-1)^i dim(C_i) = ∑_{i=0}^n (-1)^i dim(H_i)

This is a key result in algebraic topology and will be used as the
foundation for proving Euler's polyhedron formula (Wiedijk leanprover-community#13).

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>

Add the Euler-Poincaré formula proving that for bounded complexes of
finite-dimensional vector spaces, the alternating sum of dimensions
equals the alternating sum of homology dimensions.

This PR adds:
- `EulerCharacteristic.lean`: Defines Euler characteristic for chain complexes
  (adopted from PR leanprover-community#29646)
- `EulerPoincare.lean`: Proves the Euler-Poincaré formula
- Helper lemmas in `HomologicalComplex.lean` for bounded complexes

The main theorem shows that for a bounded complex C of finite-dimensional
vector spaces over a field k, if C vanishes after position n, then:
∑_{i=0}^n (-1)^i dim(C_i) = ∑_{i=0}^n (-1)^i dim(H_i)

This is a key result in algebraic topology and will be used as the
foundation for proving Euler's polyhedron formula (Wiedijk leanprover-community#13).

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>

Add the Euler-Poincaré formula proving that for bounded complexes of
finite-dimensional vector spaces, the alternating sum of dimensions
equals the alternating sum of homology dimensions.

This PR adds:
- `EulerCharacteristic.lean`: Defines Euler characteristic for chain complexes
  (adopted from PR leanprover-community#29646)
- `EulerPoincare.lean`: Proves the Euler-Poincaré formula
- Helper lemmas in `HomologicalComplex.lean` for bounded complexes

The main theorem shows that for a bounded complex C of finite-dimensional
vector spaces over a field k, if C vanishes after position n, then:
∑_{i=0}^n (-1)^i dim(C_i) = ∑_{i=0}^n (-1)^i dim(H_i)

This is a key result in algebraic topology and will be used as the
foundation for proving Euler's polyhedron formula (Wiedijk leanprover-community#13).

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>

Add the Euler-Poincaré formula proving that for bounded complexes of
finite-dimensional vector spaces, the alternating sum of dimensions
equals the alternating sum of homology dimensions.

This PR adds:
- `EulerCharacteristic.lean`: Defines Euler characteristic for chain complexes
  (adopted from PR leanprover-community#29646)
- `EulerPoincare.lean`: Proves the Euler-Poincaré formula
- Helper lemmas in `HomologicalComplex.lean` for bounded complexes

The main theorem shows that for a bounded complex C of finite-dimensional
vector spaces over a field k, if C vanishes after position n, then:
∑_{i=0}^n (-1)^i dim(C_i) = ∑_{i=0}^n (-1)^i dim(H_i)

This is a key result in algebraic topology and will be used as the
foundation for proving Euler's polyhedron formula (Wiedijk leanprover-community#13).

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>

Add the Euler-Poincaré formula proving that for bounded complexes of
finite-dimensional vector spaces, the alternating sum of dimensions
equals the alternating sum of homology dimensions.

This PR adds:
- `EulerCharacteristic.lean`: Defines Euler characteristic for chain complexes
  (adopted from PR leanprover-community#29646)
- `EulerPoincare.lean`: Proves the Euler-Poincaré formula
- Helper lemmas in `HomologicalComplex.lean` for bounded complexes

The main theorem shows that for a bounded complex C of finite-dimensional
vector spaces over a field k, if C vanishes after position n, then:
∑_{i=0}^n (-1)^i dim(C_i) = ∑_{i=0}^n (-1)^i dim(H_i)

This is a key result in algebraic topology and will be used as the
foundation for proving Euler's polyhedron formula (Wiedijk leanprover-community#13).

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>

Add the Euler-Poincaré formula proving that for bounded complexes of
finite-dimensional vector spaces, the alternating sum of dimensions
equals the alternating sum of homology dimensions.

This PR adds:
- `EulerCharacteristic.lean`: Defines Euler characteristic for chain complexes
  (adopted from PR leanprover-community#29646)
- `EulerPoincare.lean`: Proves the Euler-Poincaré formula
- Helper lemmas in `HomologicalComplex.lean` for bounded complexes

The main theorem shows that for a bounded complex C of finite-dimensional
vector spaces over a field k, if C vanishes after position n, then:
∑_{i=0}^n (-1)^i dim(C_i) = ∑_{i=0}^n (-1)^i dim(H_i)

This is a key result in algebraic topology and will be used as the
foundation for proving Euler's polyhedron formula (Wiedijk leanprover-community#13).

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>

- Add new file Mathlib/Algebra/Homology/EulerCharacteristic.lean with:
  * boundedEulerChar: bounded Euler characteristic up to index n
  * eulerChar: infinite sum Euler characteristic
  * homologyBoundedEulerChar: homological Euler characteristic
- Move chain complex helper lemmas to EulerPoincare.lean
- Add import to Mathlib.lean
- Keep HomologicalComplex.lean unchanged

This prepares for the Euler-Poincaré formula by defining the Euler
characteristic following the approach in PR leanprover-community#29646.

- Add new file Mathlib/Algebra/Homology/EulerCharacteristic.lean with:
  * boundedEulerChar: bounded Euler characteristic up to index n
  * eulerChar: infinite sum Euler characteristic
  * homologyBoundedEulerChar: homological Euler characteristic
- Prove boundedEulerChar_eq_homologyBoundedEulerChar theorem (Euler-Poincaré formula)
- Add chain complex helper lemmas to EulerPoincare.lean
- Add import to Mathlib.lean

This prepares for the Euler polyhedron formula by defining the Euler
characteristic following the approach in PR leanprover-community#29646.

- Add new file Mathlib/Algebra/Homology/EulerCharacteristic.lean with:
  * boundedEulerChar: bounded Euler characteristic up to index n
  * eulerChar: infinite sum Euler characteristic
  * homologyBoundedEulerChar: homological Euler characteristic
- Prove boundedEulerChar_eq_homologyBoundedEulerChar theorem (Euler-Poincaré formula)
- Add chain complex helper lemmas to EulerPoincare.lean
- Add import to Mathlib.lean

This prepares for the Euler polyhedron formula by defining the Euler
characteristic following the approach in PR leanprover-community#29646.

- Add new file Mathlib/Algebra/Homology/EulerCharacteristic.lean with:
  * boundedEulerChar: bounded Euler characteristic up to index n
  * eulerChar: infinite sum Euler characteristic
  * homologyBoundedEulerChar: homological Euler characteristic
- Prove boundedEulerChar_eq_homologyBoundedEulerChar theorem (Euler-Poincaré formula)
- Add chain complex helper lemmas to EulerPoincare.lean
- Add import to Mathlib.lean

This prepares for the Euler polyhedron formula by defining the Euler
characteristic following the approach in PR leanprover-community#29646.

- Add new file Mathlib/Algebra/Homology/EulerCharacteristic.lean with:
  * boundedEulerChar: bounded Euler characteristic up to index n
  * eulerChar: infinite sum Euler characteristic
  * homologyBoundedEulerChar: homological Euler characteristic
- Prove boundedEulerChar_eq_homologyBoundedEulerChar theorem (Euler-Poincaré formula)
- Add chain complex helper lemmas to EulerPoincare.lean
- Add import to Mathlib.lean for both EulerCharacteristic and EulerPoincare

This prepares for the Euler polyhedron formula by defining the Euler
characteristic following the approach in PR leanprover-community#29646.

- Add new file Mathlib/Algebra/Homology/EulerCharacteristic.lean with:
  * boundedEulerChar: bounded Euler characteristic up to index n
  * eulerChar: infinite sum Euler characteristic
  * homologyBoundedEulerChar: homological Euler characteristic
- Prove boundedEulerChar_eq_homologyBoundedEulerChar theorem (Euler-Poincaré formula)
- Add chain complex helper lemmas to EulerPoincare.lean
- Add import to Mathlib.lean for both EulerCharacteristic and EulerPoincare

This prepares for the Euler polyhedron formula by defining the Euler
characteristic following the approach in PR leanprover-community#29646.