mathlib documentation

category_theory.preadditive.opposite

If C is preadditive, Cᵒᵖ has a natural preadditive structure. #

@[simp]
@[simp]
theorem category_theory.unop_add (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] {X Y : Cᵒᵖ} (f g : X Y) :
(f + g).unop = f.unop + g.unop