Theorem FintypeCat.id_hom

Modification history

2026-03-12 17:39

Mathlib/CategoryTheory/FintypeCat.lean

refactor(CategoryTheory/FintypeCat): redefine `FintypeCat` as a full subcategory of `Type` (#36498)

Modified FintypeCat.id_hom View on Github →

2025-12-18 13:14

Mathlib/CategoryTheory/FintypeCat.lean

refactor(CategoryTheory): make morphisms in full subcategories a 1-field structure (#26446) …

Added FintypeCat.id_hom View on Github →