Theorem CategoryTheory.Discrete.hom_eq

Modification history

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 →