Theorem CategoryTheory.ProjectiveResolution.extMk_comp_mk₀

Modification history

2026-01-10 11:02
Mathlib/CategoryTheory/Abelian/Projective/Ext.lean
feat(Algebra/Homology): functoriality of `ProjectiveResolution.extMk` (#33358) …
Added CategoryTheory.ProjectiveResolution.extMk_comp_mk₀View on Github →