Documentation

Mathlib.CategoryTheory.Preadditive.SingleObj

SingleObj α is preadditive when α is a ring. #

@[instance_reducible]
Equations