Theorem PresheafOfModules.leftUnitor_inv_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.leftUnitor_inv_appView 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.leftUnitor_inv_appView on Github →