Commit 2023-05-01 22:19 4707059d

View on Github →

feat: port CategoryTheory.Functor.LeftDerived (#3751)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Functor/LeftDerived.lean

added def CategoryTheory.Functor.leftDerived

added def CategoryTheory.Functor.leftDerivedObjIso

added def CategoryTheory.Functor.leftDerivedObjProjectiveSucc

added def CategoryTheory.Functor.leftDerivedObjProjectiveZero

added theorem CategoryTheory.Functor.leftDerived_map_eq

added def CategoryTheory.NatTrans.leftDerived

added theorem CategoryTheory.NatTrans.leftDerived_comp

added theorem CategoryTheory.NatTrans.leftDerived_eq

added theorem CategoryTheory.NatTrans.leftDerived_id