SingleObj α is preadditive when α is a ring.

instance CategoryTheory.instPreadditiveSingleObjCategoryToMonoidToMonoidWithZeroToSemiring {α : Type u_1} [Ring α] : CategoryTheory.Preadditive (CategoryTheory.SingleObj α)

Equations

• CategoryTheory.instPreadditiveSingleObjCategoryToMonoidToMonoidWithZeroToSemiring = CategoryTheory.Preadditive.mk