mathlib

23d1b33c - feat(category_theory): categories where inclusions into coproducts are mono (#16867)