Commit 2021-04-23 07:17 0070d22a
View on Github →feat(algebra/category/Module): mono_iff_injective (#7100)
We should also prove epi_iff_surjective at some point. In the Module case this doesn't fall out of an adjunction, but it's still true.
feat(algebra/category/Module): mono_iff_injective (#7100)
We should also prove epi_iff_surjective at some point. In the Module case this doesn't fall out of an adjunction, but it's still true.