Theorem CochainComplex.HomComplex.CohomologyClass.bijective_toSmallShiftedHom_of_isKInjective

Modification history

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