functorCategoryPreadditive — Mathlib

Lean4
instance functorCategoryPreadditive : Preadditive (C ⥤ D)
    where
  homGroup F
    G :=
    { nsmul := nsmulRec
      zsmul := zsmulRec
      sub := fun α β => { app := fun X => α.app X - β.app X }
      add_assoc := by
        intros
        ext
        apply add_assoc
      zero_add := by
        intros
        ext
        apply zero_add
      add_zero := by
        intros
        ext
        apply add_zero
      add_comm := by
        intros
        ext
        apply add_comm
      sub_eq_add_neg := by
        intros
        ext
        apply sub_eq_add_neg
      neg_add_cancel := by
        intros
        ext
        apply neg_add_cancel }
  add_comp := by
    intros
    ext
    apply add_comp
  comp_add := by
    intros
    ext
    apply comp_add
Похожие утверждения