Theorem CochainComplex.HomComplex.CohomologyClass.bijective_toSmallShiftedHom_of_isKProjective

Modification history

2025-12-19 13:08
Mathlib/Algebra/Homology/DerivedCategory/KProjective.lean
feat(Algebra/Homology): equivOfIsKInjective (#32814) …
Added CochainComplex.HomComplex.CohomologyClass.bijective_toSmallShiftedHom_of_isKProjectiveView on Github →