Commit 2024-03-13 12:48 60ad7428

View on Github →

perf(Abelian.InjectiveResolution): refactor CochainComplex.mkAux (#11349) Similar to the changes for ChainComplex.mkAux we remove the ad-hoc MkStruct and replace with it ShortComplex.

Estimated changes

Modified Mathlib/Algebra/Homology/HomologicalComplex.lean

deleted def CochainComplex.MkStruct.flat

deleted structure CochainComplex.MkStruct

modified def CochainComplex.mkAux

Modified Mathlib/CategoryTheory/Abelian/InjectiveResolution.lean