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.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
