mathlib

31019c25 - feat(category_theory/idempotents): an equivalence of categories for homological complexes (#17569)

feat(category_theory/idempotents): an equivalence of categories for homological complexes (#17569) This PR constructs an equivalence of categories `karoubi_homological_complex_equivalence C c : karoubi (homological_complex C c) ≌ homological_complex (karoubi C) c`. The automation for `karoubi` categories is also made better by the introduction of the simp lemma `karoubi.comp_f`.