Def CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv

Modification history

2024-04-25 15:18

Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean

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

Added CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv View on Github →