Commit 2024-06-10 18:57 69fa1737

View on Github →

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

Estimated changes

Modified Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean

added theorem CategoryTheory.LocallyDiscrete.eqToHom_toLoc

added theorem CategoryTheory.OplaxFunctor.map₂_eqToHom

modified theorem Quiver.Hom.comp_toLoc

modified theorem Quiver.Hom.id_toLoc

modified def Quiver.Hom.toLoc