Theorem CategoryTheory.Presheaf.freeYonedaHomEquiv_symm_comp

Modification history

2024-12-24 23:17
Mathlib/CategoryTheory/Generator/Presheaf.lean
feat(CategoryTheory/Sites): categories of sheaves have a separator (#19979) …
Added CategoryTheory.Presheaf.freeYonedaHomEquiv_symm_compView on Github →