Theorem CategoryTheory.CatEnriched.id_eq

Modification history

2025-12-17 16:11
Mathlib/CategoryTheory/Bicategory/CatEnriched.lean
feat(CategoryTheory/Cat/Basic): Turning 1- and 2-morphisms in Cat into a 1-field structure (#31807) …
Modified CategoryTheory.CatEnriched.id_eqView on Github →
2025-07-12 12:51
Mathlib/CategoryTheory/Bicategory/CatEnriched.lean
feat(Bicategory/CatEnriched): 2-cat from Cat-enriched cat (#25784) …
Added CategoryTheory.CatEnriched.id_eqView on Github →