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

Commit

3 years ago

feat(algebra/category/Module): upgrade `free : Type ⥤ Module R` to a monoidal functor (#14328) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author

kim-em

Parents

9229b0e0

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

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