Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-04 14:08 343237d1

View on Github →

feat(algebra/Module): the category of R-modules (#1420)

  • Adds Module category
  • Move punit module instance to punit_instances.lean
  • Minor formatting
  • Use coercions for Module morphisms to functions
  • Small formatting improvements to Module
  • Move module_id to id_apply
  • Be specific about the universe Modules live in
  • Minor indentation formatting
  • updates for #1380
  • oops
  • remove ext lemma, unnecessary
  • reverting changes in TopCommRing
  • Change name of module_hom_comp Co-Authored-By: Johan Commelin johan@commelin.net
  • Update todo in src/algebra/category/Module/basic.lean Co-Authored-By: Scott Morrison scott@tqft.net

Estimated changes