Theorem PresheafOfModulesOfCommRing.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)

Added PresheafOfModulesOfCommRing.leftUnitor_inv_app View on Github →