Theorem PresheafOfModules.freeYoneda.isSeparating

Modification history

2025-10-27 15:31
Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean
refactor(CategoryTheory/Generator): use ObjectProperty instead of Set (#30269) …
Modified PresheafOfModules.freeYoneda.isSeparatingView on Github →
2024-11-14 20:21
Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean
feat(Algebra/Category/ModuleCat/Presheaf): presheaves of modules are generated by their sections (#18160) …
Added PresheafOfModules.freeYoneda.isSeparatingView on Github →