mathlib documentation

category_theory.preadditive.single_obj

single_obj α is preadditive when α is a ring. #