SingleObj α is preadditive when α is a ring.

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

Equations

• CategoryTheory.instPreadditiveSingleObjCategoryToMonoidToMonoidWithZeroToSemiring = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }