Mathlib v3 is deprecated. Go to Mathlib v4

Def Module.monoidal_free

Modification history

2022-07-01 04:21

src/algebra/category/Module/adjunctions.lean

feat(algebra/category/Module): upgrade `free : Type ⥤ Module R` to a monoidal functor (#14328)

Added Module.monoidal_free View on Github →