Mathlib Changelog
v4
Changelog
About
Github
Theorem
CochainComplex.isSplitMono_from_singleFunctor_obj_of_injective
Modification history
2025-04-28 06:56
Mathlib/Algebra/Homology/DerivedCategory/Ext/EnoughInjectives.lean
feat(CategoryTheory/Abelian): Ext when there are enough injectives (#23797) …
Added
CochainComplex.isSplitMono_from_singleFunctor_obj_of_injective
View on Github →