Theorem CochainComplex.IsKProjective.Qh_map_bijective

Modification history

2025-12-19 13:08
Mathlib/Algebra/Homology/DerivedCategory/KProjective.lean
feat(Algebra/Homology): equivOfIsKInjective (#32814) …
Modified CochainComplex.IsKProjective.Qh_map_bijectiveView on Github →
2025-12-12 17:04
Mathlib/Algebra/Homology/DerivedCategory/KProjective.lean
feat(Algebra/Homology): K-projective cochain complexes (#32741) …
Added CochainComplex.IsKProjective.Qh_map_bijectiveView on Github →