Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-20 00:16 c9c9fa15

View on Github →

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

Estimated changes