Def CategoryTheory.Discrete.discreteCases

Modification history

2025-11-19 06:07
Mathlib/CategoryTheory/Discrete/Basic.lean
chore: move Mathlib to the module system (#31786) …
Deleted CategoryTheory.Discrete.discreteCasesView on Github →
2023-06-07 05:59
Mathlib/CategoryTheory/DiscreteCategory.lean
feat: port CategoryTheory.Monoidal.Mon_ (#4763)
Added CategoryTheory.Discrete.discreteCasesView on Github →