Theorem CategoryTheory.InjectiveResolution.Hom.ι'_comp_hom'

Modification history

2026-01-16 21:23

Mathlib/CategoryTheory/Abelian/Injective/Extend.lean

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

Added CategoryTheory.InjectiveResolution.Hom.ι'_comp_hom'View on Github →