Theorem PresheafOfModules.Elements.fromFreeYoneda_app_apply

Modification history

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.Elements.fromFreeYoneda_app_applyView on Github →