mathlib3 documentation

category_theory.abelian.functor_category

If D is abelian, then the functor category C ⥤ D is also abelian. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.