Theorem PresheafOfModulesOfCommRing.naturality_apply

Modification history

2026-09-05 01:44

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

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

Added PresheafOfModulesOfCommRing.naturality_apply View on Github →