Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-20 12:24 c66c4afa

View on Github →

chore(algebra/Module/monoidal): add the simp lemmas for unitors and associativity (#2196)

  • feat(algebra/category/Module/monoidal): simp lemmas
  • oops
  • depressingly easy
  • order of arguments

Estimated changes

deleted def Module.of_self