Preadditive

Statistics

Metric	Count
Definitions	0
Theorems `liftNatTrans_add`, `liftNatTrans_zero`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`liftNatTrans_add` 📖	mathematical	—	`liftNatTrans` `Quiver.Hom` `CategoryTheory.Functor` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.instAddHomFunctor`	—	`natTrans_ext` `liftNatTrans_app` `CategoryTheory.Preadditive.add_comp` `CategoryTheory.Preadditive.comp_add`
`liftNatTrans_zero` 📖	mathematical	—	`liftNatTrans` `Quiver.Hom` `CategoryTheory.Functor` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Limits.instHasZeroMorphismsFunctor`	—	`natTrans_ext` `liftNatTrans_app` `CategoryTheory.Limits.zero_comp` `CategoryTheory.Limits.comp_zero`

---