Theorem CategoryTheory.ProjectiveResolution.Hom.hom_comp_π

Modification history

2026-01-16 21:23

Mathlib/CategoryTheory/Preadditive/Projective/Resolution.lean

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

Added CategoryTheory.ProjectiveResolution.Hom.hom_comp_π View on Github →