Theorem HomologicalComplex.restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv

Modification history

2025-01-16 22:07
Mathlib/Algebra/Homology/Embedding/TruncGE.lean
feat(Algebra/Homology/Embedding): the morphism from a complex to its `truncGE` truncation (#19544) …
Added HomologicalComplex.restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_invView on Github →