Theorem CategoryTheory.shrinkYonedaEquiv_shrinkYoneda_map

Modification history

2025-12-11 08:08
Mathlib/CategoryTheory/ShrinkYoneda.lean
feat(CategoryTheory): the Yoneda embedding for a locally small category (#32424) …
Added CategoryTheory.shrinkYonedaEquiv_shrinkYoneda_mapView on Github →