Theorem FintypeCat.Skeleton.incl_mk_nat_card

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.Skeleton.incl_mk_nat_card View on Github →

2023-04-10 19:55

Mathlib/CategoryTheory/FintypeCat.lean

feat: port CategoryTheory.Fintype (#3365)

Added FintypeCat.Skeleton.incl_mk_nat_card View on Github →