Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-03 16:19 0ac3f9d2

View on Github →

feat(category_theory/preadditive): the category of additive functors (#12330)

Estimated changes

Modified src/category_theory/preadditive/additive_functor.lean

added def category_theory.AdditiveFunctor.forget

added theorem category_theory.AdditiveFunctor.forget_map

added theorem category_theory.AdditiveFunctor.forget_obj

added theorem category_theory.AdditiveFunctor.forget_obj_of

added def category_theory.AdditiveFunctor.of

added theorem category_theory.AdditiveFunctor.of_fst

added def category_theory.AdditiveFunctor