DerivedCountCoproduct.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.derivedCountCoproductIsColimit line 23
Source documentation
The original count direct sum, with its original inclusions, is an actual coproduct after passing to the genuine integer derived category.
```
def derivedCountCoproductIsColimit :
    IsColimit ((integerQ D).mapCocone (directSumComplexCocone D S)) := by
…
```
Mentions: OAI.DerivedBar.integerQ, OAI.DerivedBar.directSumComplexCocone