2022-03-17 07:17
src/category_theory/abelian/injective_resolution.lean
feat(category_theory/abelian/injective_resolution): homotopy between descents of morphism and two injective resolutions (#12743) …
Added category_theory.InjectiveResolution.homotopy_equiv_hom_ι