mathlib3 documentation

category_theory.preadditive.single_obj

`single_obj α` is preadditive when `α` is a ring. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[protected, instance]

def category_theory.single_obj.preadditive {α : Type u_1} [ring α] :

category_theory.preadditive (category_theory.single_obj α)

Equations

category_theory.single_obj.preadditive = {hom_group := λ (P Q : category_theory.single_obj α), non_unital_non_assoc_ring.to_add_comm_group (P ⟶ Q), add_comp' := _, comp_add' := _}