Theorem PresheafOfModules.Sheafify.map_smul_eq

Modification history

2026-03-06 08:34
Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean
refactor(CategoryTheory/Sites): redefine the category of sheaves using `ObjectProperty.FullSubcategory` (#36081) …
Modified PresheafOfModules.Sheafify.map_smul_eqView on Github →
2024-06-06 20:44
Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean
feat: the associated sheaf of a presheaf of modules (#11555) …
Added PresheafOfModules.Sheafify.map_smul_eqView on Github →