Mathlib v3 is deprecated. Go to Mathlib v4

Theorem category_theory.AdditiveFunctor.forget_obj_of

Modification history

2022-03-03 16:19
src/category_theory/preadditive/additive_functor.lean
feat(category_theory/preadditive): the category of additive functors (#12330)
Added category_theory.AdditiveFunctor.forget_obj_ofView on Github →