Theorem HomologicalComplex.truncGEMap_id

Modification history

2024-11-30 00:03
Mathlib/Algebra/Homology/Embedding/TruncGE.lean
feat(Algebra/Homology/Embedding): the canonical truncation functor `trunGEFunctor` (#19543) …
Added HomologicalComplex.truncGEMap_idView on Github →