Commit 2026-04-30 19:12 3dcb295b

View on Github →

chore(Algebra/Homology/HomologicalComplex): make CochainComplex.of and ChainComplex.of abbrevs (#38661) This PR changes ChainComplex.of and CochainComplex.of into abbrevs so that the following example would work:

example : (ChainComplex.of X d ..).X n = X n := by with_reducible rfl

which allows us to apply Finsupp lemmas on (inhomogeneousChains M).X n that fixes the issue in #38553.

Estimated changes

deleted def ChainComplex.of
modified theorem ChainComplex.of_d
modified theorem ChainComplex.of_d_ne
deleted def CochainComplex.of
modified theorem CochainComplex.of_d
modified theorem CochainComplex.of_d_ne