mathlib3

6af5fbd2 - feat(category_theory/.../zero): if a zero morphism is a mono, the source is zero (#7462)

feat(category_theory/.../zero): if a zero morphism is a mono, the source is zero (#7462) Some simple lemmas about zero morphisms. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>