mathlib

c9c9fa15 - refactor(category_theory/discrete): make discrete irreducible (#13762)

refactor(category_theory/discrete): make discrete irreducible (#13762) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Adam Topaz <github@adamtopaz.com> Co-authored-by: Jakob von Raumer <jakob@von-raumer.de> Co-authored-by: Markus Himmel <markus@himmel-villmar.de> Co-authored-by: yuma-mizuno <mizuno.y.aj@gmail.com> Co-authored-by: Praneeth Kolichala <praneeth.kolichala@gmail.com>