PR #2125 feat(algebra): monoidal category of R-modules

feat(algebra): monoidal category of R-modules #2125

mergify merged 11 commits into master from monoidal_Module

feat(algebra): monoidal category of R-modules

2806d684

docstrings

6a2fc6f9

minor

eadb5587

tweaks

6c9166ed

fix import

7095bb23

jcommelin commented on 2020-03-11

fixes

554a33bc

reduce use of @

9691c2fe

jcommelin added WIP

broken

8e0281f7

fixes

45d6f28c

kim-em removed WIP

kim-em added awaiting-review

jcommelin approved these changes on 2020-03-14

jcommelin removed awaiting-review

jcommelin added ready-to-merge

bryangingechen commented on 2020-03-14

Merge branch 'master' into monoidal_Module

6d62981a

Update src/algebra/category/Module/basic.lean

73b03e70

mergify merged 81d3ebf3 into master 6 years ago

mergify deleted the monoidal_Module branch 6 years ago

Reviewers

jcommelin

bryangingechen

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone