Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-14 08:02 81d3ebf3

View on Github →

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

Estimated changes