Theorem PresheafOfModules.tensorHom_app

Modification history

2026-09-05 01:44

Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean

feat(Algebra/Category/ModuleCat): refactor Monoidal.lean to use `PresheafOfModulesOfCommRing` (#43193)

Deleted PresheafOfModules.tensorHom_app View on Github →

2026-04-04 12:29

Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean

feat(Algebra/Category/ModuleCat): the category of presheaves of modules is symmetric (#37370) …

Added PresheafOfModules.tensorHom_app View on Github →