Commit 2024-12-20 17:17 74c027f0

View on Github →

feat(Algebra/Homology): the stupid truncation of homological complexes (#18501)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Homology/Embedding/Basic.lean

Modified Mathlib/Algebra/Homology/Embedding/Extend.lean

Created Mathlib/Algebra/Homology/Embedding/StupidTrunc.lean

added theorem HomologicalComplex.isZero_stupidTrunc_X

added theorem HomologicalComplex.isZero_stupidTrunc_iff

added theorem HomologicalComplex.stupidTruncMap_comp

added theorem HomologicalComplex.stupidTruncMap_id

added theorem HomologicalComplex.stupidTruncMap_stupidTruncXIso_hom