Mathlib v3 is deprecated. Go to Mathlib v4

Def Module.normal_mono

Modification history

2020-08-03 11:29
src/algebra/category/Module/abelian.lean
feat(algebra/category/Group): the category of abelian groups is abelian (#3621)
Modified Module.normal_monoView on Github →
2020-08-03 05:29
src/algebra/category/Module/abelian.lean
feat(algebra/category/Module): the category of R-modules is abelian (#3606)
Added Module.normal_monoView on Github →