Module R #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file shows that an
R-linear map is a monomorphism in the category of
if and only if it is injective, and similarly an epimorphism if and only if it is surjective.
If the zero morphism is an epi then the codomain is trivial.