Def Module.of_hom

Modification history

2022-03-12 11:37
src/algebra/category/Module/basic.lean
chore(algebra/category/Module): remove unnecessary universe restriction (#12610)
Modified Module.of_homView on Github →
2021-10-01 03:25
src/algebra/category/Module/basic.lean
chore(algebra/category/*): Added `of_hom` to all of the algebraic categories. (#9454) …
Added Module.of_homView on Github →