SingleObj α
is preadditive when α
is a ring. #
instance
CategoryTheory.instPreadditiveSingleObjCategoryToMonoidToMonoidWithZeroToSemiring
{α : Type u_1}
[Ring α]
:
Equations
- CategoryTheory.instPreadditiveSingleObjCategoryToMonoidToMonoidWithZeroToSemiring = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }