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.