Theorem HomologicalComplex.isSeparator_coproduct_separatingFamily

Modification history

2025-02-24 12:08
Mathlib/CategoryTheory/Generator/HomologicalComplex.lean
feat(CategoryTheory): categories of homological complexes have a separator (#20229) …
Added HomologicalComplex.isSeparator_coproduct_separatingFamilyView on Github →