Theorem CategoryTheory.map_shrinkYonedaEquiv

Modification history

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