Theorem CategoryTheory.Discrete.id_def'

Modification history

2026-08-15 18:18
Mathlib/CategoryTheory/Discrete/Basic.lean
chore(CategoryTheory/Discrete/Basic): refactor the hom type for `to_dual` (#42796) …
Modified CategoryTheory.Discrete.id_def'View on Github →
2025-11-01 00:46
Mathlib/CategoryTheory/Discrete/Basic.lean
feat(CategoryTheory): (Co)limits in preorders (#29253) …
Added CategoryTheory.Discrete.id_def'View on Github →