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.

Estimated changes