Theorem CategoryTheory.InjectiveResolution.mk₀_comp_extMk

Modification history

2026-10-18 07:19

Mathlib/CategoryTheory/Abelian/Injective/Ext.lean

feat(Category/Abelian/Injective): interaction between `InjectiveResolution.extMk` and the connecting morphism (#43224) …

Modified CategoryTheory.InjectiveResolution.mk₀_comp_extMk View on Github →

2026-01-10 11:02

Mathlib/CategoryTheory/Abelian/Injective/Ext.lean

feat(Algebra/Homology): functoriality of `ProjectiveResolution.extMk` (#33358) …

Added CategoryTheory.InjectiveResolution.mk₀_comp_extMk View on Github →