Documentation

Mathlib.CategoryTheory.Preadditive.SingleObj

SingleObj α is preadditive when α is a ring. #

Equations
  • CategoryTheory.instPreadditiveSingleObj = { homGroup := inferInstance, add_comp := , comp_add := }