Theorem CategoryTheory.AdditiveFunctor.forget_obj_of

Modification history

2023-03-11 13:48
Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean
feat: port CategoryTheory.Preadditive.AdditiveFunctor (#2779)
Added CategoryTheory.AdditiveFunctor.forget_obj_ofView on Github →