Commit 2024-09-24 12:27 c01c9ce0

View on Github →

feat(CategoryTheory): The whiskering functor preserves identity and composition of functors (#16971)

Estimated changes

Modified Mathlib/CategoryTheory/Whiskering.lean

added def CategoryTheory.whiskeringLeftObjCompIso

added def CategoryTheory.whiskeringLeftObjIdIso

added theorem CategoryTheory.whiskeringLeft_obj_comp

added theorem CategoryTheory.whiskeringLeft_obj_id

added def CategoryTheory.whiskeringRightObjCompIso

added theorem CategoryTheory.whiskeringRight_obj_comp

added theorem CategoryTheory.whiskeringRight_obj_id

added def CategoryTheory.wiskeringRightObjIdIso