Theorem CategoryTheory.LocallyDiscrete.mk_as

Modification history

2024-04-25 15:18

Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean

feat(CategoryTheory/Bicategory/LocallyDiscrete): Make LocallyDiscrete a structure (#12383) …

Added CategoryTheory.LocallyDiscrete.mk_as View on Github →