Commit 2025-02-07 17:17 dbf8ce9b

View on Github →

feat(Algebra/Homology): the alternating constant complex (#21558)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Fin.lean

added theorem Fin.sum_neg_one_pow

Created Mathlib/Algebra/Homology/AlternatingConst.lean

added def ChainComplex.alternatingConst

added def ChainComplex.alternatingConstHomologyDataEvenNEZero

added def ChainComplex.alternatingConstHomologyDataOdd

added def ChainComplex.alternatingConstHomologyDataZero

added def ChainComplex.alternatingConstHomologyZero

added theorem ChainComplex.isZero_alternatingConst_homology

Modified Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean

added def AlgebraicTopology.alternatingFaceMapComplexConst