Commit 2023-02-11 14:37 21ba5902

View on Github →

feat: Port/category theory.functor.const (#2208) Very straightforward port. Almost completely automatic!

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Functor/Const.lean

added def CategoryTheory.Functor.const.opObjOp

added def CategoryTheory.Functor.const.opObjUnop

added theorem CategoryTheory.Functor.const.opObjUnop_hom_app

added theorem CategoryTheory.Functor.const.opObjUnop_inv_app

added theorem CategoryTheory.Functor.const.unop_functor_op_obj_map

added def CategoryTheory.Functor.const

added def CategoryTheory.Functor.constComp