Def CategoryTheory.Core.inclusionCompFunctorToCoreIso

Modification history

2025-11-04 23:41

Mathlib/CategoryTheory/Core.lean

feat(CategoryTheory): naturality lemmas for Core construction (#29284) …

Added CategoryTheory.Core.inclusionCompFunctorToCoreIso View on Github →