Commit 2025-04-04 06:55 a38bc397

View on Github →

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

Estimated changes

Modified Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean

Modified Mathlib/CategoryTheory/Whiskering.lean

added def CategoryTheory.whiskeringRightObjIdIso

deleted def CategoryTheory.wiskeringRightObjIdIso