mathlib3
74333bd5 - feat(category_theory): is_zero.op and is_zero.unop (#17718)

Commit

3 years ago

feat(category_theory): is_zero.op and is_zero.unop (#17718) This PR shows that a zero object is also a zero object in the opposite category.

Author

joelriou

Parents