Commit 2024-01-08 23:13 49dcbe7d
View on Github →perf (Homology.ProjectiveResolution): remove MkStruct, re-jigger proof, and suppress compilation (#9555)
Currently CategoryTheory.Abelian.ProjectiveResolution requires more than double the next largest file in terms of CPU instructions. This reduces the load by replacing ad-hoc MkStruct with ShortComplex and pushing around the existing proof. Follow-up clean-up should be done.