Def CategoryTheory.LocallyDiscrete

Modification history

2024-04-25 15:18
Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean
feat(CategoryTheory/Bicategory/LocallyDiscrete): Make LocallyDiscrete a structure (#12383) …
Deleted CategoryTheory.LocallyDiscreteView on Github →
2023-03-13 13:46
Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean
feat: port CategoryTheory.Bicategory.LocallyDiscrete (#2813)
Added CategoryTheory.LocallyDiscreteView on Github →