Theorem CategoryTheory.Discrete.Hom.eq'

Modification history

2026-10-04 06:22
Mathlib/CategoryTheory/Discrete/Basic.lean
feat(Translate): command for adding a translation (#43750) …
Deleted CategoryTheory.Discrete.Hom.eq'View on Github →
2026-08-15 18:18
Mathlib/CategoryTheory/Discrete/Basic.lean
chore(CategoryTheory/Discrete/Basic): refactor the hom type for `to_dual` (#42796) …
Added CategoryTheory.Discrete.Hom.eq'View on Github →