Def CategoryTheory.wiskeringRightObjIdIso

Modification history

2025-04-04 06:55

Mathlib/CategoryTheory/Whiskering.lean

chore(CategoryTheory/Whiskering): fix typos (#23647)

Deleted CategoryTheory.wiskeringRightObjIdIso View on Github →

2024-09-24 12:27

Mathlib/CategoryTheory/Whiskering.lean

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

Added CategoryTheory.wiskeringRightObjIdIso View on Github →