Theorem Quiver.Hom.id_toLoc

Modification history

2024-06-10 18:57

Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean

feat(Bicategory/LocallyDiscrete): add eqToHom lemmas (#13695)

Modified Quiver.Hom.id_toLoc View on Github →

2024-04-25 15:18

Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean

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

Added Quiver.Hom.id_toLoc View on Github →