Mathlib v3 is deprecated. Go to Mathlib v4

Def category_theory.AdditiveFunctor.forget

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 View on Github →