feat(algebra): monoidal category of R-modules (#2125)
* feat(algebra): monoidal category of R-modules
* docstrings
* minor
* tweaks
* fix import
* fixes
* reduce use of @
* broken
* fixes
* Update src/algebra/category/Module/basic.lean
Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
