Theorem CochainComplex.mappingCone.inr_f_descShortComplex_f

Modification history

2024-06-24 10:09
Mathlib/Algebra/Homology/HomotopyCategory/ShortExact.lean
feat: the mapping cone of a monomorphism, up to a quasi-isomorphism (#13675) …
Added CochainComplex.mappingCone.inr_f_descShortComplex_fView on Github →