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