Theorem CategoryTheory.ProjectiveResolution.Hom.hom'_comp_π'

Modification history

2026-01-16 21:23

Mathlib/CategoryTheory/Abelian/Projective/Extend.lean

feat(Algebra/Homology): functoriality of `extMk` with respect to the injective resolution (#33360) …

Added CategoryTheory.ProjectiveResolution.Hom.hom'_comp_π'View on Github →