Theorem PresheafOfModulesOfCommRing.tensorObj_obj

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.tensorObj_obj View on Github →