Mathlib v3 is deprecated. Go to Mathlib v4

Def Module.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)

Modified Module.free.μ View on Github →

2021-10-21 02:55

src/algebra/category/Module/adjunctions.lean

chore(*): bump to lean 3.34.0 (#9824) …

Added Module.free.μ View on Github →