Theorem CochainComplex.isKProjective_iff_leftOrthogonal

Modification history

2025-12-12 17:04
Mathlib/Algebra/Homology/HomotopyCategory/KProjective.lean
feat(Algebra/Homology): K-projective cochain complexes (#32741) …
Added CochainComplex.isKProjective_iff_leftOrthogonalView on Github →