Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-01 04:21 7e244d8b

View on Github →

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

Estimated changes

added theorem Module.free.ε_apply
modified def Module.free.μ