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