Theorem CategoryTheory.CatEnrichedOrdinary.id_eq_eqToHom

Modification history

2025-12-13 14:21
Mathlib/CategoryTheory/Bicategory/CatEnriched.lean
chore: use `Category*` everywhere (#32842) …
Modified CategoryTheory.CatEnrichedOrdinary.id_eq_eqToHomView on Github →
2025-07-12 12:51
Mathlib/CategoryTheory/Bicategory/CatEnriched.lean
feat(Bicategory/CatEnriched): 2-cat from Cat-enriched cat (#25784) …
Added CategoryTheory.CatEnrichedOrdinary.id_eq_eqToHomView on Github →