SingleObj α is preadditive when α is a ring. #
Equations
- CategoryTheory.instPreadditiveSingleObj = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }
SingleObj α is preadditive when α is a ring. #