Theorem HomologicalComplex.truncGE'Map_f_eq_opcyclesMap

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.truncGE'Map_f_eq_opcyclesMapView on Github →